Revision #1262 → #2286 · back to history
addedGroup presentation2846f9441d80
modifiedHyperbolic groupa9cb61ae7102
| Field | From #1262 | To #2286 |
|---|
| note | Mathlib's only 'hyperbolic' references are to hyperbolic functions/geometry, not Gromov-hyperbolic groups. | Mathlib's only 'hyperbolic' references are to hyperbolic functions/geometry and `Matrix.IsHyperbolic`, not Gromov-hyperbolic groups. |
modifiedGromov's polynomial growth theorema65f1757253b
| Field | From #1262 | To #2286 |
|---|
| note | No formalization of group growth or Gromov's theorem exists (the only 'polynomial growth' is Akra–Bazzi function asymptotics). | No formalization of group growth or Gromov's theorem exists in Mathlib. |
modifiedMostow rigidity theoreme09a5cb295ea
| Field | From #1262 | To #2286 |
|---|
| note | Mostow rigidity is not present in Mathlib. | Mostow rigidity is not present in Mathlib (loogle returns zero hits for 'Mostow'). |
addedDehn function / isoperimetric function7214b9441a2e
addedKazhdan's property (T)f7c76292a9d0
addedBass–Serre theory5519795f7242
modifiedAmenable groups53e3668e776c
| Field | From #1262 | To #2286 |
|---|
| note | Mathlib has Følner-filter amenability (`IsFoelner.amenable`) but, per its own docstring, no standalone definition of an amenable group. | Mathlib has Følner-filter amenability (`IsFoelner.amenable`) but no standalone definition of an amenable group as a class. |
modifiedOuter automorphism groups Out(Fn)0d03171d0742
| Field | From #1262 | To #2286 |
|---|
| note | Mathlib has `MulAut` and `FreeGroup` but no outer automorphism group (Aut/Inn) construction. | Mathlib has `MulAut` and `FreeGroup` but no `OuterAut`/Out(Fn) construction (loogle returns zero 'OuterAut' hits). |
modifiedBraid groupsb0964e3ff52b
| Field | From #1262 | To #2286 |
|---|
| note | Mathlib's 'braid' references are to braided monoidal categories, not the braid groups. | Mathlib's 'braid'/'braiding' references are all to braided monoidal categories, not the Artin braid groups Bn. |
modifiedBaumslag–Solitar groupsf3939a5a2244
| Field | From #1262 | To #2286 |
|---|
| note | Baumslag–Solitar groups are HNN extensions of ℤ; Mathlib has the general `HNNExtension` construction but not these specific groups. | Baumslag–Solitar groups are HNN extensions of ℤ; Mathlib has the general `HNNExtension` construction but not these specific groups (loogle returns zero 'BaumslagSolitar' hits). |
modifiedGrigorchuk group8f80adcf2e64
| Field | From #1262 | To #2286 |
|---|
| note | The Grigorchuk group is not formalized in Mathlib. | The Grigorchuk group is not formalized in Mathlib (loogle returns zero 'Grigorchuk' hits). |