mathlib4

mathlib4 copied to clipboard

feat(SetTheory/Cardinal/Regular): define singular cardinals

1

Define singular cardinals and prove basic lemmas about them. --- [](https://gitpod.io/from-referrer/)

YnirPaz

chore: refactor algebraic filter bases

1

--- [](https://gitpod.io/from-referrer/)

ADedecker

feat(NumberTheory/NumberField): proof of the Analytic Class Number Formula

2

--- - [ ] depends on: #16675 - [x] depends on: #16822 - [ ] depends on: #12488 - [ ] depends on: #12405 - [x] depends on: #17943 -...

xroblot

chore(Order/Intervals/Set): move some defs to a new file

5

--- [](https://gitpod.io/from-referrer/)

urkud

feat(Analysis/Normed/Group/SeparationQuotient): add normed lifts and `mk`

1

Define the `mk` and lifts of normed spaces and normed groups by the inseparable setoid as `NormedAddGroupHom`, `CLM`, etc. Motivation: In the GNS representation, operators in the original C^*-algebra are...

yoh-tanimoto

RFC/chore(Algebra/GCDMonoid): should we un-`@[simp]` normalize_apply?

2

The lemma `normalize_apply` feels to me like it exposes the implementation detail that `normalize` is defined in terms of `normUnit`. I think the `normalize` function itself is much more familiar...

Vierkantor

feat(SetTheory/Cardinal/Basic): out_lift_equiv

8

Prove `out_lift_equiv`. --- [](https://gitpod.io/from-referrer/)

YnirPaz

feat: virtually nilpotent groups

3

Show that nilpotency is preserved under group isomorphisms and define virtually nilpotent subgroups. From GrowthInGroups --- [](https://gitpod.io/from-referrer/)

YaelDillies

feat(Archive/Imo): formalize IMO 1982q1

4

Formalized question 1 of the 1982 IMO. Made a mistake with my original PR as I made a branch from Imo1982Q3, this should be fixed now. Fixed the domain of...

AlexBrodbelt

feat(Ideal/IsPrincipalPowQuotient): R/I equiv I^n/I^(n+1)

3

--- [](https://gitpod.io/from-referrer/)

pechersky