coeFun — Mathlib

English

There is a canonical coercion from a unitary group element to the matrix it represents, i.e., a unitary matrix is identified with its entries in M_n(α).

Русский

Существует каноническое отображение из элемента группы унитарных матриц в соответствующую матрицу, то есть унитарная матрица идентифицируется с её элементами в M_n(α).

LaTeX

$$$\\text{coercion}: \\mathrm{unitaryGroup}(n,\\alpha) \\to (\\mathrm{Matrix}(n,n,\\alpha))$, $A \\mapsto A_1$.$$

Lean4

instance coeFun : CoeFun (unitaryGroup n α) fun _ => n → n → α where coe A := A.val

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