mathlib3
9720321c - rm finite_groups (will be a different PR to make the PR smaller)

Commit

3 years ago

rm finite_groups (will be a different PR to make the PR smaller)

References

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

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

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

Author

matthias567

matthias567

Parents

Loading