mathlib3
feat (group_theory/amenable) : Folner sequences, Folner amenability, example integers
#16581
Open
Open
feat (group_theory/amenable) : Folner sequences, Folner amenability, example integers #16581
matthias567
wants to merge
8 commits into
master
from
amenable_groups-fol
feat (group_theory/amenable) : define amenable groups
a5314494
feat (group_theory/amenable) : Finite groups are amenable.
b7a63e49
fix authors (s missing)
2b096c84
feat (group_theory/amenable) : Folner sequences, Folner amenability, …
5dced829
rm superfluous aux_lemma_sums
6879c71d
feat (group_theory/amenable) : Folner sequences, Folner amenability, …
0d2aa8cf
restructure, rm aux_lemmas (already exist in mathlib)
c1737ab1
Merge branch 'amenable_groups-fol' of github.com:leanprover-community…
7abc8223
Reviewers
No reviews
Assignees
No one assigned
Labels
awaiting-review
blocked-by-other-PR
too-late
Milestone
No milestone
Login to write a write a comment.
Login via GitHub