@[reducible, inline]

abbrev GroupCounts.G₂₄ : Type

theorem GroupCounts.G₂₄_inv_eq_self (a : G₂₄) : a⁻¹ = a

noncomputable def GroupCounts.subgroupToFinset₂₄ (H : Subgroup G₂₄) : Finset G₂₄

theorem GroupCounts.subgroupToFinset₂₄_mem (H : Subgroup G₂₄) (g : G₂₄) : g ∈ subgroupToFinset₂₄ H ↔ g ∈ H

theorem GroupCounts.subgroupToFinset₂₄_card (H : Subgroup G₂₄) : (subgroupToFinset₂₄ H).card = Nat.card ↥H

theorem GroupCounts.natcard_G₂₄ : Nat.card G₂₄ = 16

theorem GroupCounts.index_eq_two_iff_card_eq_eight (H : Subgroup G₂₄) : H.index = 2 ↔ Nat.card ↥H = 8

theorem GroupCounts.subgroupToFinset₂₄_is_carrier (H : Subgroup G₂₄) : 1 ∈ subgroupToFinset₂₄ H ∧ ∀ a ∈ subgroupToFinset₂₄ H, ∀ b ∈ subgroupToFinset₂₄ H, a * b ∈ subgroupToFinset₂₄ H

noncomputable def GroupCounts.finsetToSubgroup₂₄ (s : Finset G₂₄) (h1 : 1 ∈ s) (hmul : ∀ a ∈ s, ∀ b ∈ s, a * b ∈ s) : Subgroup G₂₄

theorem GroupCounts.round_trip_finset₂₄ (s : Finset G₂₄) (h1 : 1 ∈ s) (hmul : ∀ a ∈ s, ∀ b ∈ s, a * b ∈ s) : subgroupToFinset₂₄ (finsetToSubgroup₂₄ s h1 hmul) = s

theorem GroupCounts.round_trip_subgroup₂₄ (H : Subgroup G₂₄) : finsetToSubgroup₂₄ (subgroupToFinset₂₄ H) ⋯ ⋯ = H

def GroupCounts.subgroupCarriersIdx2 : Finset (Finset G₂₄)

theorem GroupCounts.subgroupCarriersIdx2_card : subgroupCarriersIdx2.card = 15

theorem GroupCounts.mem_subgroupCarriersIdx2 (s : Finset G₂₄) : s ∈ subgroupCarriersIdx2 ↔ 1 ∈ s ∧ (∀ a ∈ s, ∀ b ∈ s, a * b ∈ s) ∧ s.card = 8

noncomputable def GroupCounts.subgroupIdx2Equiv : { H : Subgroup G₂₄ // H.index = 2 } ≃ ↥subgroupCarriersIdx2

theorem GroupCounts.Z2Z4_index2_count : Nat.card { H : Subgroup (Multiplicative (ZMod 2 × ZMod 2 × ZMod 2 × ZMod 2)) // H.index = 2 } = 15

@[reducible, inline]

abbrev GroupCounts.G₄₃ : Type

def GroupCounts.addHomTriple (a b c : ZMod 4) : ZMod 4 × ZMod 4 × ZMod 4 →+ ZMod 4

def GroupCounts.mulHomTriple (a b c : ZMod 4) : G₄₃ →* Multiplicative (ZMod 4)

theorem GroupCounts.mem_ker_mulHomTriple (a b c : ZMod 4) (g : G₄₃) : g ∈ (mulHomTriple a b c).ker ↔ a * (Multiplicative.toAdd g).1 + b * (Multiplicative.toAdd g).2.1 + c * (Multiplicative.toAdd g).2.2 = 0

def GroupCounts.isSurjTriple (a b c : ZMod 4) : Prop

theorem GroupCounts.mulHomTriple_surjective (a b c : ZMod 4) (h : isSurjTriple a b c) : Function.Surjective ⇑(mulHomTriple a b c)

theorem GroupCounts.mulHomTriple_ker_index (a b c : ZMod 4) (h : isSurjTriple a b c) : (mulHomTriple a b c).ker.index = 4

theorem GroupCounts.mulHomTriple_ker_isCyclic (a b c : ZMod 4) (h : isSurjTriple a b c) : IsCyclic (G₄₃ ⧸ (mulHomTriple a b c).ker)

theorem GroupCounts.addHom_eq_triple (f : ZMod 4 × ZMod 4 × ZMod 4 →+ ZMod 4) (x y z : ZMod 4) : f (x, y, z) = f (1, 0, 0) * x + f (0, 1, 0) * y + f (0, 0, 1) * z

theorem GroupCounts.mulHom_eq_triple (f : G₄₃ →* Multiplicative (ZMod 4)) : ∃ (a : ZMod 4) (b : ZMod 4) (c : ZMod 4), ∀ (g : G₄₃), f g = (mulHomTriple a b c) g

noncomputable def GroupCounts.subgroupToFinset₄₃ (H : Subgroup G₄₃) : Finset G₄₃

theorem GroupCounts.subgroupToFinset₄₃_mem (H : Subgroup G₄₃) (g : G₄₃) : g ∈ subgroupToFinset₄₃ H ↔ g ∈ H

theorem GroupCounts.subgroupToFinset₄₃_injective : Function.Injective subgroupToFinset₄₃

theorem GroupCounts.natcard_G₄₃ : Nat.card G₄₃ = 64

def GroupCounts.kerFinsetMul (a b c : ZMod 4) : Finset G₄₃

def GroupCounts.surjKernelsMul : Finset (Finset G₄₃)

theorem GroupCounts.surjKernelsMul_card : surjKernelsMul.card = 28

theorem GroupCounts.ker_carrier_eq_kerFinsetMul (a b c : ZMod 4) : subgroupToFinset₄₃ (mulHomTriple a b c).ker = kerFinsetMul a b c

theorem GroupCounts.ker_carrier_mem_surjKernels (a b c : ZMod 4) (h : isSurjTriple a b c) : subgroupToFinset₄₃ (mulHomTriple a b c).ker ∈ surjKernelsMul

noncomputable def GroupCounts.surjTripleOf (s : Finset G₄₃) (hs : s ∈ surjKernelsMul) : { abc : ZMod 4 × ZMod 4 × ZMod 4 // isSurjTriple abc.1 abc.2.1 abc.2.2 ∧ s = kerFinsetMul abc.1 abc.2.1 abc.2.2 }

theorem GroupCounts.carrier_of_cyclic_idx4_in_surjKernels (H : Subgroup G₄₃) (hidx : H.index = 4) (hcyc : IsCyclic (G₄₃ ⧸ H)) : subgroupToFinset₄₃ H ∈ surjKernelsMul

noncomputable def GroupCounts.subgroupCyclicIdx4Equiv : { H : Subgroup G₄₃ // H.index = 4 ∧ IsCyclic (G₄₃ ⧸ H) } ≃ ↥surjKernelsMul

theorem GroupCounts.Z4Z3_cyclic_quartic_count : Nat.card { H : Subgroup (Multiplicative (ZMod 4 × ZMod 4 × ZMod 4)) // H.index = 4 ∧ IsCyclic (Multiplicative (ZMod 4 × ZMod 4 × ZMod 4) ⧸ H) } = 28