mathlib
a5314494 - feat (group_theory/amenable) : define amenable groups

Commit

3 years ago

feat (group_theory/amenable) : define amenable groups We define amenable groups, via the existence of left-invariant means. The structure mean in defined in 'mean', and 'def_amenable' adds the condition on left invariance.

References

#16574 - feat (group_theory/amenable) : define amenable groups

#16575 - feat (group_theory/amenable) : Quotients of amenable groups are amenable

#16576 - feat (group_theory/amenable) : Subgroups of Amenable Groups are Amenable

#16578 - feat (group_theory/amenable) : Extensions of Amenable groups are amenable

#16580 - feat (group_theory/amenable): Free groups are not amenable

#16581 - feat (group_theory/amenable) : Folner sequences, Folner amenability, example integers

#16695 - feat (group_theory/amenable) : Finite groups are amenable

Author

matthias567

Parents

a547b3b3

mathlib a5314494 - feat (group_theory/amenable) : define amenable groups

mathlib
a5314494 - feat (group_theory/amenable) : define amenable groups