toGL — Mathlib

English

The map toGL sends a unitary matrix to its general linear group isomorphism representation via the corresponding linear equivalence.

Русский

Векторное отображение toGL отправляет унитарную матрицу в соответствующее отображение GL через линейное эквивалентность.

LaTeX

$$toGL(A) = GeneralLinearGroup.ofLinearEquiv (toLinearEquiv(A))$$

Lean4

/-- `Matrix.unitaryGroup.toGL` is the map from the unitary group to the general linear group -/
def toGL (A : unitaryGroup n α) : GeneralLinearGroup α (n → α) :=
  GeneralLinearGroup.ofLinearEquiv (toLinearEquiv A)

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