semidirectProductMulEquiv — Mathlib

English

The group associated to a split extension is isomorphic to a semidirect product: E ≅ N ⋊[s.conjAct] G.

Русский

Группа, связанная с разложенным расширением, изоморфна полусоединённому произведению: E ≅ N ⋊[s.conjAct] G.

LaTeX

$$$ (N \\rtimes[ s.conjAct ] G) \\cong* E $$$

Lean4

/-- The group associated to a split extension is isomorphic to a semidirect product. -/
noncomputable def semidirectProductMulEquiv : N ⋊[s.conjAct] G ≃* E :=
  s.semidirectProductToGroupExtensionEquiv.toMulEquiv

Похожие утверждения