Groups of order 10

TheoremNoncyclic groups of order 10 are dihedral#✓fully proved

Every finite group of order \(10\) that is not cyclic is isomorphic to the dihedral group \(D_5\) of order \(10\).

theorem nonempty_mulEquiv_dihedralGroup_of_card_eq_ten_of_not_isCyclic
    (G : Type*) [Group G] [Fintype G] (hG : Fintype.card G = 10) (hnc : ¬IsCyclic G) :
    Nonempty (G ≃* DihedralGroup 5)

Sources

the generators and inversion argument are adapted from the archived AlgebraNotes source; the final isomorphism uses the shared index-two constructor.

Uses 1 · Used by 1

Proof usesDihedral groups from a cyclic subgroup of index two

Used byClassification of groups of order 10

TheoremClassification of groups of order 10#✓fully proved

Every finite group of order \(10\) is isomorphic either to the cyclic group \(C_{10}\) of order \(10\) or to the dihedral group \(D_5\) of order \(10\).

theorem groups_of_order_10_classification
    (G : Type*) [Group G] [Fintype G] (hG : Fintype.card G = 10) :
    Nonempty (G ≃* Multiplicative (ZMod 10)) ∨ Nonempty (G ≃* DihedralGroup 5)

Uses 1 · Used by 2

Proof usesNoncyclic groups of order 10 are dihedral

Used byClassification of groups of order 10, product form · Exclusive classification of groups of order 10

TheoremExclusive classification of groups of order 10#✓fully proved

Let \(G\) be a finite group of order \(10\). Then exactly one of the following holds: \(G\) is isomorphic to the cyclic group \(C_{10}\) of order \(10\), or \(G\) is isomorphic to the dihedral group \(D_5\) of order \(10\).

The two alternatives cannot both hold, since \(C_{10}\) is cyclic, \(D_5\) is not, and cyclicity is preserved under isomorphism.

theorem groups_of_order_10_classification_xor
    (G : Type*) [Group G] [Fintype G] (hG : Fintype.card G = 10) :
    (Nonempty (G ≃* Multiplicative (ZMod 10)) ∧ ¬Nonempty (G ≃* DihedralGroup 5)) ∨
      (¬Nonempty (G ≃* Multiplicative (ZMod 10)) ∧ Nonempty (G ≃* DihedralGroup 5))

Uses 1

Proof usesClassification of groups of order 10

TheoremClassification of groups of order 10, product form#✓fully proved

Let \(C_n\) denote the cyclic group of order \(n\) and let \(D_5\) denote the dihedral group of order \(10\). Every finite group of order \(10\) is isomorphic to the direct product \(C_5 \times C_2\) or to \(D_5\).

theorem groups_of_order_10_classification_prod
    (G : Type*) [Group G] [Fintype G] (hG : Fintype.card G = 10) :
    Nonempty (G ≃* (Multiplicative (ZMod 5) × Multiplicative (ZMod 2))) ∨
      Nonempty (G ≃* DihedralGroup 5)

Uses 1 · Used by 1

Proof usesClassification of groups of order 10

Used byExclusive classification of groups of order 10, product form

TheoremExclusive classification of groups of order 10, product form#✓fully proved

Let \(G\) be a finite group of order \(10\), let \(C_n\) denote the cyclic group of order \(n\), and let \(D_5\) denote the dihedral group of order \(10\). Then exactly one of the following holds: \(G\) is isomorphic to the direct product \(C_5 \times C_2\), or \(G\) is isomorphic to \(D_5\).

The product \(C_5 \times C_2\) is cyclic and \(D_5\) is not, so the two alternatives cannot both hold.

theorem groups_of_order_10_classification_prod_xor
    (G : Type*) [Group G] [Fintype G] (hG : Fintype.card G = 10) :
    (Nonempty (G ≃* (Multiplicative (ZMod 5) × Multiplicative (ZMod 2))) ∧
      ¬Nonempty (G ≃* DihedralGroup 5)) ∨
    (¬Nonempty (G ≃* (Multiplicative (ZMod 5) × Multiplicative (ZMod 2))) ∧
      Nonempty (G ≃* DihedralGroup 5))

Uses 1

Proof usesClassification of groups of order 10, product form

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.