def Hex.PermGroup.DirectProduct.equiv {n m : ℕ} (G : Group n) (H : Group m) : Element (G.directProduct H) ≃* Element G × Element H

The executable factor projections identify the checked group with the mathematical direct product, preserving multiplication.

Equations

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

@[simp]

theorem Hex.PermGroup.DirectProduct.equiv_pair {n m : ℕ} (G : Group n) (H : Group m) (p : Element G) (q : Element H) : (equiv G H) (pair p q) = (p, q)

def Hex.PermGroup.DirectProduct.inlHom {n m : ℕ} (G : Group n) (H : Group m) : Element G →* Element (G.directProduct H)

Equations

• Hex.PermGroup.DirectProduct.inlHom G H = { toFun := Hex.PermGroup.DirectProduct.inl H, map_one' := ⋯, map_mul' := ⋯ }

def Hex.PermGroup.DirectProduct.inrHom {n m : ℕ} (G : Group n) (H : Group m) : Element H →* Element (G.directProduct H)

Equations

• Hex.PermGroup.DirectProduct.inrHom G H = { toFun := Hex.PermGroup.DirectProduct.inr G, map_one' := ⋯, map_mul' := ⋯ }

def Hex.PermGroup.DirectProduct.fstHom {n m : ℕ} (G : Group n) (H : Group m) : Element (G.directProduct H) →* Element G

Equations

• Hex.PermGroup.DirectProduct.fstHom G H = (MonoidHom.fst (Hex.PermGroup.Element G) (Hex.PermGroup.Element H)).comp (Hex.PermGroup.DirectProduct.equiv G H).toMonoidHom

def Hex.PermGroup.DirectProduct.sndHom {n m : ℕ} (G : Group n) (H : Group m) : Element (G.directProduct H) →* Element H

Equations

• Hex.PermGroup.DirectProduct.sndHom G H = (MonoidHom.snd (Hex.PermGroup.Element G) (Hex.PermGroup.Element H)).comp (Hex.PermGroup.DirectProduct.equiv G H).toMonoidHom

def Hex.PermGroup.DirectProduct.groupEquiv {n m : ℕ} (G : Group n) (H : Group m) : ↥(closure (G.directProduct H).generators) ≃* ↥(closure G.generators) × ↥(closure H.generators)

The same multiplicative equivalence stated entirely in Mathlib subgroups.

Equations

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

theorem Hex.PermGroup.DirectProduct.groupEquiv_pair {n m : ℕ} (G : Group n) (H : Group m) (p : Element G) (q : Element H) : (groupEquiv G H) ((Element.equiv (G.directProduct H)) (pair p q)) = ((Element.equiv G) p, (Element.equiv H) q)

theorem Hex.PermGroup.DirectProduct.groupEquiv_apply {n m : ℕ} (G : Group n) (H : Group m) (r : Element (G.directProduct H)) : (groupEquiv G H) ((Element.equiv (G.directProduct H)) r) = ((Element.equiv G) (fst r), (Element.equiv H) (snd r))

The Mathlib equivalence uses exactly the executable coordinate projections.