toLinearMap_inj — Mathlib

English

Equality of the underlying linear maps implies equality of the semilinear equivalences.

Русский

Равенство базовых линейных отображений влечет равенство семилинейных эквивалентностей.

LaTeX

$$$(↑e_1 : M \to M_2) = e_2 \iff e_1 = e_2$$$

Lean4

@[simp, norm_cast]
theorem toLinearMap_inj {e₁ e₂ : M ≃ₛₗ[σ] M₂} : (↑e₁ : M →ₛₗ[σ] M₂) = e₂ ↔ e₁ = e₂ :=
  toLinearMap_injective.eq_iff

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