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

Commits
  • feat (group_theory/amenable) : define amenable groups
    matthias567 committed 3 years ago
  • feat (group_theory/amenable) : Finite groups are amenable.
    matthias567 committed 3 years ago
  • fix authors (s missing)
    matthias567 committed 3 years ago
  • feat (group_theory/amenable) : Folner sequences, Folner amenability, example integers
    matthias567 committed 3 years ago
  • rm superfluous aux_lemma_sums
    matthias567 committed 3 years ago
  • feat (group_theory/amenable) : Folner sequences, Folner amenability, example integers
    matthias567 committed 3 years ago
  • restructure, rm aux_lemmas (already exist in mathlib)
    matthias567 committed 3 years ago
  • Merge branch 'amenable_groups-fol' of github.com:leanprover-community/mathlib into amenable_groups-fol
    matthias567 committed 3 years ago
Loading