Elementary abelian groups of order 4

An additive commutative group of cardinality four that is a ZMod 2-module is a Klein four-group.

A commutative group of order 4 whose maximal elementary-2 quotient G / G² has 2-rank 2 is as large as that quotient, so every element squares to one (TauCeti.sq_eq_one_of_card_elementaryTwoQuotient_eq_card) and G is a Klein four-group.

Main results

• TauCeti.isAddKleinFour_of_natCard_eq_four: a ZMod 2-module of cardinality four is a Klein four-group.
• TauCeti.isKleinFour_of_card_eq_four_of_twoRank_eq_two: such a group is a Klein four-group.

theorem TauCeti.isAddKleinFour_of_natCard_eq_four {A : Type u_1} [AddCommGroup A] [Module (ZMod 2) A] (hcard : Nat.card A = 4) : IsAddKleinFour A

An additive commutative group of cardinality four that is a ZMod 2-module is a Klein four-group.

theorem TauCeti.isKleinFour_of_card_eq_four_of_twoRank_eq_two {G : Type u_1} [CommGroup G] (hcard : Nat.card G = 4) (hrank : twoRank G = 2) : IsKleinFour G

A commutative group of order 4 and 2-rank 2 is a Klein four-group. Its maximal elementary-2 quotient has 2 ^ 2 = 4 elements, as many as G, so G has exponent 2.