May I add `Equiv.Perm.center_eq_bot` to Mathlib?

Stream: new members

[Alissa Tung]

Hello, when using Mathlib, I noticed that there doesn't seem to be a theorem stating that when $3 \leq n$, we have Subgroup.center (Equiv.Perm (Fin n)) = ⊥. May I add this theorem to Mathlib? If so, could you also grant my GitHub account alissa-tung membership in the lean-community organization?

[Luigi Massacci]

If no one adds you soon-ish, ask in #mathlib4 > github permission. As for the theorem, I wonder whether it's worth to prove it for any permutation group of cardinality >= 3, and not just the finite ones. The proof is the same anyway