def Hex.PermGroup.Group.index {n : Nat} (G H : Group n) (_h : H.IsSubgroup G) : Nat

The exact index for a contained subgroup. Integrality follows from the transversal product decomposition, not from truncated division alone.

Equations

• G.index H _h = G.order / H.order

theorem Hex.PermGroup.LeftTransversal.count {n : Nat} {G H : Group n} (t : LeftTransversal G H) (h : H.IsSubgroup G) : t.reps.size = G.index H h

theorem Hex.PermGroup.LeftTransversal.disjoint {n : Nat} {G H : Group n} (t : LeftTransversal G H) {i j : Fin t.reps.size} (hne : i ≠ j) (p : Perm n) : ¬(Generated H.generators (t.reps[↑i].val.inv.comp p) ∧ Generated H.generators (t.reps[↑j].val.inv.comp p))

Distinct stored cosets share no permutation, even if H is not normal.

theorem Hex.PermGroup.Group.exists_transversal {n : Nat} (G H : Group n) : Nonempty (LeftTransversal G H)

theorem Hex.PermGroup.Group.index_mul_order {n : Nat} (G H : Group n) (h : H.IsSubgroup G) : G.index H h * H.order = G.order

theorem Hex.PermGroup.Group.index_pos {n : Nat} (G H : Group n) (h : H.IsSubgroup G) : 0 < G.index H h

theorem Hex.PermGroup.Group.coset_count {n : Nat} (G H : Group n) (h : H.IsSubgroup G) (c : Action.Orbit G (LeftCoset H)) (hc : Action.Orbit.Valid (Action.leftCosets G H) (LeftCoset.mk H (Perm.id n)) c) : c.objects.size = G.index H h

theorem Hex.PermGroup.Group.cosetLimit_false {n : Nat} (G H : Group n) (h : H.IsSubgroup G) (e : (Action.leftCosets G H).OrbitLimit (LeftCoset.mk H (Perm.id n)) (G.index H h)) : False

def Hex.PermGroup.Group.leftTransversal {n : Nat} (G H : Group n) (h : H.IsSubgroup G) : LeftTransversal G H

Traverse the coset orbit with precisely the known index as capacity. The public wrapper checks the caller's cap before invoking this helper.

Equations

• One or more equations did not get rendered due to their size.

def Hex.PermGroup.Group.leftCosetsCapped {n : Nat} (cap : Nat) (G H : Group n) (h : H.IsSubgroup G) : Except SizeLimit (LeftTransversal G H)

Complete deterministic left transversal, or an exact size-limit result before allocation. The representatives need not be canonical across inputs.

Equations

• Hex.PermGroup.Group.leftCosetsCapped cap G H h = if G.index H h ≤ cap then Except.ok (G.leftTransversal H h) else Except.error { required := G.index H h, capacity := cap }

theorem Hex.PermGroup.Group.leftCosetsCapped_ok {n : Nat} (cap : Nat) (G H : Group n) (h : H.IsSubgroup G) : (∃ (t : LeftTransversal G H), leftCosetsCapped cap G H h = Except.ok t) ↔ G.index H h ≤ cap

theorem Hex.PermGroup.Group.leftCosetsCapped_error {n : Nat} (cap : Nat) (G H : Group n) (h : H.IsSubgroup G) : leftCosetsCapped cap G H h = Except.error { required := G.index H h, capacity := cap } ↔ cap < G.index H h

theorem Hex.PermGroup.Group.leftCosetsCapped_spec {n : Nat} (cap : Nat) (G H : Group n) (h : H.IsSubgroup G) (t : LeftTransversal G H) (ht : leftCosetsCapped cap G H h = Except.ok t) : t.reps.size = G.index H h ∧ t.reps.size ≤ cap ∧ G.order = t.reps.size * H.order