mathlib3

feat (group_theory/amenable) : Finite groups are amenable

#16695

Open