mulEquivProd — Mathlib

English

There is a group isomorphism between the semidirect product N ⋊[1] G and the direct product N × G, where the action φ is trivial.

Русский

Существует изоморфизм групп между полупрямым произведением N ⋊[1] G и прямым произведением N × G, когда действие тривиально.

LaTeX

$$$ N \rtimes_{1} G \cong^* N \times G $$$

Lean4

/-- The group isomorphism between a semidirect product with respect to the trivial map
  and the product. -/
@[simps (rhsMd := .default)]
def mulEquivProd : N ⋊[1] G ≃* N × G :=
  { equivProd with map_mul' _ _ := rfl }

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