feat(GroupTheory/SpecificGroups): define an isomorphism between a non-cyclic group of order 4 and the dihedral group of order 4

[wupr]

---

This was suggested in a comment on #7937.

[wupr]

I wasn't sure where to place this definition. I imagine further classification of finite groups of small order would probably justify a dedicated "Mathlib/GroupTheory/SpecificGroups/SmallOrder.lean".

[wupr]

A note on the final simp. I added (config := { decide := true }) because replacing it with (config := { decide := false }) would fail to close the goal, and if I'm understanding correctly, the forthcoming change (leanprover/lean4#2722) in Lean v4.4.0 would break the proof.

[j-loreaux]

I have thoughts about this, please don't merge yet.

[j-loreaux]

I've just opened #8565, which I think may be the way we actually want to go about this (it implements @jcommelin suggestion from #7937 in this comment). With #8565, the result in this PR can be obtained as follows:

import Mathlib.GroupTheory.SpecificGroups.KleinFour

variable {G : Type} [Group G] [Fintype G]

/-- A non-cyclic group of order 4 is isomorphic to the dihedral group of order 4. -/
noncomputable def mulEquivOfCardEqFourAndNotIsCyclic (h1 : Fintype.card G = 4) (h2 : ¬IsCyclic G) :
    DihedralGroup 2 ≃* G :=
  IsKleinFour.mulEquiv' ((Fintype.equivOfCardEq h1.symm : DihedralGroup 2 ≃ G).setValue 1 1)
    (by simp) <| (IsKleinFour.not_isCyclic_iff h1).mp h2

[wupr]

Thanks @j-loreaux . I might just move my def to KleinFour.lean once #8565 is merge. A lemma to similar effect has been added to #8565 after discussion with the author.

[wupr]

I'm closing this PR in favour of #8565.