embeddingGL — Mathlib

English

The embedding embeddingGL is a monoid homomorphism from the unitary group to GL.

Русский

Вложение embeddingGL является гомоморфизмом моноида от унитарной группы к GL.

LaTeX

$$embeddingGL : unitaryGroup n α →* GeneralLinearGroup α (n → α)$$

Lean4

/-- `Matrix.unitaryGroup.embeddingGL` is the embedding from `Matrix.unitaryGroup n α` to
`LinearMap.GeneralLinearGroup n α`. -/
def embeddingGL : unitaryGroup n α →* GeneralLinearGroup α (n → α) :=
  ⟨⟨fun A => toGL A, toGL_one⟩, toGL_mul⟩

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