instGroup — Mathlib

English

The semidirect product N ⋊φ G carries a group structure (with the stated multiplication).

Русский

У полупрямого произведения N ⋊φ G имеется структура группы (с указанным законом умножения).

LaTeX

$$$\\text{SemidirectProduct}(N,G,\\phi) \\, \\text{is a group}$$$

Lean4

instance : Group (N ⋊[φ] G)
    where
  mul_assoc a b c := SemidirectProduct.ext (by simp [mul_assoc]) (by simp [mul_assoc])
  one_mul a := SemidirectProduct.ext (by simp) (one_mul a.2)
  mul_one a := SemidirectProduct.ext (by simp) (mul_one _)
  inv_mul_cancel a := SemidirectProduct.ext (by simp) (by simp)

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