toGLPos — Mathlib

English

The embedding from SpecialLinearGroup to GLPos is injective: distinct special linear matrices map to distinct GLPos elements.

Русский

Встраивание из SL(n, R) в GL^+(n, R) инъективно: разные матрицы с det 1 переходят в разные элементы GL^+(n, R).

LaTeX

$$$\text{toGLPos}: SL(n,R) \to GL^+_n(R) \text{ is injective},$ i.e. $toGLPos(A)=toGLPos(B) \Rightarrow A=B$.$$

Lean4

/-- `Matrix.SpecialLinearGroup n R` embeds into `GL_pos n R` -/
def toGLPos : SpecialLinearGroup n R →* GLPos n R
    where
  toFun A := ⟨(A : GL n R), show 0 < (↑A : Matrix n n R).det from A.prop.symm ▸ zero_lt_one⟩
  map_one' := Subtype.ext <| Units.ext <| rfl
  map_mul' _ _ := Subtype.ext <| Units.ext <| rfl

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