mathlib3

feat (group_theory/amenable): Free groups are not amenable

#16580

Open