The Klein four reference permutation group in degree four

The reference subgroup of 4T2 is Mathlib's alternatingGroup.kleinFour (Fin 4), the normal subgroup of A₄ made of the identity and the three double transpositions, viewed inside Equiv.Perm (Fin 4). We record that it is a Klein four-group, so that every permutation group with label 4T2 is one. The converse for transitive subgroups of S₄ is TauCeti.transitiveGroupLabel_four_one_iff_isKleinFour, in TauCeti.GroupTheory.Perm.TransitiveGroupLabel.Order.

Main declarations

• TauCeti.isKleinFour_referenceSubgroup_four_one: the reference subgroup of 4T2 is a Klein four-group.
• TauCeti.TransitiveGroupLabel.isKleinFour_four_one: a permutation group with label 4T2 is a Klein four-group.

instance TauCeti.isKleinFour_referenceSubgroup_four_one : IsKleinFour ↥(referenceSubgroup 4 ⟨1, isKleinFour_referenceSubgroup_four_one._proof_1⟩)

The reference subgroup of 4T2 is a Klein four-group.

theorem TauCeti.TransitiveGroupLabel.isKleinFour_four_one {G : Subgroup (Equiv.Perm (Fin 4))} (h : TransitiveGroupLabel ⟨1, isKleinFour_referenceSubgroup_four_one._proof_1⟩ G) : IsKleinFour ↥G

Every permutation group with label 4T2 is a Klein four-group.