mathlib3
c1737ab1 - restructure, rm aux_lemmas (already exist in mathlib)

Commit

3 years ago

restructure, rm aux_lemmas (already exist in mathlib)

References

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

Author

matthias567

matthias567

Parents

Loading