toLin'_injective — Mathlib

English

The map toLin' is injective on SpecialLinearGroup n R.

Русский

Карта toLin' инъективна на группе SpecialLinearGroup n R.

LaTeX

$$Function.Injective toLin' : SpecialLinearGroup n R →* (n → R) ≃ₗ[R] n → R$$

Lean4

theorem toLin'_injective : Function.Injective ↑(toLin' : SpecialLinearGroup n R →* (n → R) ≃ₗ[R] n → R) := fun _ _ h =>
  Subtype.coe_injective <| Matrix.toLin'.injective <| LinearEquiv.toLinearMap_injective.eq_iff.mpr h

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