specialUnitaryGroup — Mathlib

English

The function representation of 1 in the unitary group is the identity matrix.

Русский

Функциональное отображение единицы из унитарной группы является тождественной матрицей.

LaTeX

$$$\\uparrow(1 : unitaryGroup n α) = I_n$$$

Lean4

/-- `Matrix.specialUnitaryGroup` is the group of unitary `n` by `n` matrices where the determinant
is 1. (This definition is only correct if 2 is invertible.) -/
def specialUnitaryGroup : Submonoid (Matrix n n α) :=
  unitaryGroup n α ⊓ MonoidHom.mker detMonoidHom

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