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

Open

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

matthias567 wants to merge 6 commits into master from amenable_groups-ext

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) : Quotients of amenable groups are amena…

640d1e87

feat (group_theory/amenable) : Subgroups of amenable groups are amena…

b88b078c

feat (group_theory/amenable) : Extensions of amenable groups are amen…

48e5c997

matthias567 added awaiting-review

mathlib-dependent-issues-bot added blocked-by-other-PR

kim-em added too-late

Reviewers

No reviews

Assignees

No one assigned

Labels

awaiting-review blocked-by-other-PR too-late

Milestone

No milestone