toLinearEquiv_injective — Mathlib

English

A simplified form that the same injectivity holds for the specialized coe map.

Русский

Упрощённая форма того, что инъективность сохраняется для специализированного коe отображения.

LaTeX

$$$ (\uparrow) \text{ is injective } $$$

Lean4

theorem toLinearEquiv_injective : Function.Injective (toLinearEquiv : (M₁ ≃SL[σ₁₂] M₂) → M₁ ≃ₛₗ[σ₁₂] M₂) :=
  by
  rintro ⟨e, _, _⟩ ⟨e', _, _⟩ rfl
  rfl

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