toGL — Mathlib

English

There is a canonical monoid hom from the special linear group to the general linear group, sending each matrix with determinant 1 to its underlying invertible matrix.

Русский

Существует каноническое моноидное отображение из SpecialLinearGroup в GeneralLinearGroup, отправляющее каждую матрицу с детерминантом 1 в соответствующую обратимую матрицу.

LaTeX

$$\\text{toGL} : \\mathrm{SL}_n(R) \\to \\mathrm{GL}_n(R)$$

Lean4

/-- `toGL` is the map from the special linear group to the general linear group. -/
def toGL : Matrix.SpecialLinearGroup n R →* Matrix.GeneralLinearGroup n R
    where
  toFun A := ⟨↑A, ↑A⁻¹, congr_arg (·.1) (mul_inv_cancel A), congr_arg (·.1) (inv_mul_cancel A)⟩
  map_one' := Units.ext rfl
  map_mul' _ _ := Units.ext rfl

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