mathlib3

feat (group_theory/amenable) : define amenable groups

#16574

Open