def Hex.PermGroup.Normal.check {n : Nat} (G H : Group n) : Bool

Normality checked on symmetric generators already certified in the ambient chain. The checker does not run the generator normalization producer.

Equations

• Hex.PermGroup.Normal.check G H = decide (∀ (i : Fin G.chain.generators.size) (j : Fin H.generators.size), H.contains (G.chain.generators[↑i].conj H.generators[↑j]) = true)

def Hex.PermGroup.Normal.failure? {n : Nat} (G H : Group n) : Option (Fin G.chain.generators.size × Fin H.generators.size)

A full pass stops at the first failed conjugate. The nested scans do not allocate the Cartesian product of the generator arrays.

Equations

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

theorem Hex.PermGroup.Normal.failure_none {n : Nat} (G H : Group n) : failure? G H = none ↔ check G H = true

theorem Hex.PermGroup.Normal.failure_sound {n : Nat} (G H : Group n) (i : Fin G.chain.generators.size) (j : Fin H.generators.size) (h : failure? G H = some (i, j)) : ¬Generated H.generators (G.chain.generators[↑i].conj H.generators[↑j])

theorem Hex.PermGroup.Normal.check_iff {n : Nat} (G H : Group n) : check G H = true ↔ ∀ (g p : Perm n), Generated G.generators g → Generated H.generators p → Generated H.generators (g.conj p)

theorem Hex.PermGroup.Normal.check_normal {n : Nat} (G H : Group n) (h : H.IsSubgroup G) : check G H = true ↔ H.isNormal G h = true