Revision #2286 → #2953 · back to history
modifiedGeometric group theory797ca6d202a9
| Field | From #2286 | To #2953 |
|---|
| note | The field itself is not formalized, but its central object—finitely generated groups—is captured by the `Group.FG` class. | The field itself is not formalized, but its central object—finitely generated groups—is captured by the `Group.FG` typeclass. |
modifiedCayley graph and word metric9cbd480ce7f3
| Field | From #2286 | To #2953 |
|---|
| note | `SimpleGraph.mulCayley` directly defines the Cayley graph from a generating set, though the word metric is not separately packaged. | `SimpleGraph.mulCayley s` defines the Cayley graph from a generating set, though the word metric is not separately packaged. |
modifiedGromov's polynomial growth theorema65f1757253b
| Field | From #2286 | To #2953 |
|---|
| note | No formalization of group growth or Gromov's theorem exists in Mathlib. | No formalization of group growth or Gromov's polynomial growth theorem exists in Mathlib. |
modifiedStallings' ends theoremb5d6bcd95dfb
| Field | From #2286 | To #2953 |
|---|
| note | Neither the ends of groups nor Stallings' theorem is formalized. | Neither the ends of groups nor Stallings' theorem is formalized in Mathlib. |
modifiedMostow rigidity theoreme09a5cb295ea
| Field | From #2286 | To #2953 |
|---|
| note | Mostow rigidity is not present in Mathlib (loogle returns zero hits for 'Mostow'). | Mostow rigidity is not present in Mathlib. |
modifiedDehn function / isoperimetric function7214b9441a2e
| Field | From #2286 | To #2953 |
|---|
| note | Dehn functions of finitely presented groups are not formalized in Mathlib (loogle returns zero 'Dehn' hits). | Dehn functions of finitely presented groups are not formalized in Mathlib. |
modifiedKazhdan's property (T)f7c76292a9d0
| Field | From #2286 | To #2953 |
|---|
| note | Kazhdan's property (T) for discrete groups is not formalized in Mathlib (loogle returns zero 'Kazhdan' hits). | Kazhdan's property (T) for discrete groups is not formalized in Mathlib. |
modifiedAmenable groups53e3668e776c
| Field | From #2286 | To #2953 |
|---|
| note | Mathlib has Følner-filter amenability (`IsFoelner.amenable`) but no standalone definition of an amenable group as a class. | Mathlib has the Følner-filter amenability theorem (`IsFoelner.amenable`) but no standalone `Amenable` group typeclass. |
modifiedFree productsec8063f3611f
| Field | From #2286 | To #2953 |
|---|
| note | `Monoid.CoprodI` is the free product (coproduct) of a family of groups, with binary `Monoid.Coprod` as a special case. | `Monoid.CoprodI` is the free product (coproduct) of a family of groups. |
modifiedOuter automorphism groups Out(Fn)0d03171d0742
| Field | From #2286 | To #2953 |
|---|
| note | Mathlib has `MulAut` and `FreeGroup` but no `OuterAut`/Out(Fn) construction (loogle returns zero 'OuterAut' hits). | Mathlib has `MulAut` and `FreeGroup` but no `OuterAut`/Out(Fn) construction. |
modifiedMapping class groups19c36facf34d
| Field | From #2286 | To #2953 |
|---|
| note | Mapping class groups of surfaces are not formalized. | Mapping class groups of surfaces are not formalized in Mathlib. |
modifiedGeneral Artin groups694a3995d4e6
| Field | From #2286 | To #2953 |
|---|
| note | Artin groups are not defined; Mathlib only mentions the 'Artin–Tits relation' in a comment within the Coxeter files. | Artin groups are not defined; Mathlib only mentions the 'Artin–Tits relation' in comments in the Coxeter files. |
modifiedFuchsian and Kleinian groups7fbc36da0d22
| Field | From #2286 | To #2953 |
|---|
| note | Neither Fuchsian nor Kleinian groups are formalized. | Neither Fuchsian nor Kleinian groups are formalized in Mathlib. |
modifiedBaumslag–Solitar groupsf3939a5a2244
| Field | From #2286 | To #2953 |
|---|
| note | Baumslag–Solitar groups are HNN extensions of ℤ; Mathlib has the general `HNNExtension` construction but not these specific groups (loogle returns zero 'BaumslagSolitar' hits). | Baumslag–Solitar groups are HNN extensions of ℤ; Mathlib has the general `HNNExtension` construction but not these specific groups. |
modifiedGrigorchuk group8f80adcf2e64
| Field | From #2286 | To #2953 |
|---|
| note | The Grigorchuk group is not formalized in Mathlib (loogle returns zero 'Grigorchuk' hits). | The Grigorchuk group is not formalized in Mathlib. |
addedSmall cancellation theory9d25437ff190
addedvan Kampen diagramsc0592fa66305
addedBaum–Connes conjecture2290acc2a6b9
addedNovikov conjectureeb0ef012cb86
addedBurnside problem226d7c07edc2
addedGrowth rate of a finitely generated groupc14bf79ecf3e
addedNumber of ends of a group99124bc7c4fb
addedAsymptotic dimension31feb705a4be