coeMatrix — Mathlib

English

Every unitary n×n matrix over α is a matrix in M_n(α); there is a natural inclusion map from the unitary group to the full matrix ring.

Русский

Каждая унитарная матрица размерности n×n над α является матрицей в M_n(α); имеется естественное включение унитарной группы в полный матричный круг.

LaTeX

$$$\\iota: \\mathrm{unitaryGroup}(n,\\alpha) \\to \\mathrm{Matrix}(n,n,\\alpha),\\quad \\iota(A) = A_1.$$$

Lean4

instance coeMatrix : Coe (unitaryGroup n α) (Matrix n n α) :=
  ⟨Subtype.val⟩

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