toGLPos_injective — Mathlib

English

The map toGLPos from SpecialLinearGroup to GLPos is injective; i.e., if toGLPos(A)=toGLPos(B) then A=B.

Русский

Отображение toGLPos из SL(n,R) в GL^+(n,R) инъективно; если toGLPos(A)=toGLPos(B), то A=B.

LaTeX

$$$toGLPos: SL(n,R) \to GL^+_n(R)$ is injective; $toGLPos(A)=toGLPos(B) \Rightarrow A=B$.$$

Lean4

theorem toGLPos_injective : Function.Injective (toGLPos : SpecialLinearGroup n R → GLPos n R) :=
  -- Porting note: had to rewrite this to hint the correct types to Lean
    -- (It can't find the coercion GLPos n R → Matrix n n R)

  Function.Injective.of_comp (f := fun (A : GLPos n R) ↦ ((A : GL n R) : Matrix n n R)) Subtype.coe_injective

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