coe_inj — Mathlib

English

The coercion from ContinuousLinearMap to its underlying semilinear map is injective; two maps are equal iff their underlying semilinear maps are equal.

Русский

Приведение из непрерывного линейного отображения к его базовой семилинейной карте является инъекцией; два отображения равны тогда и только тогда, когда равны их базовые семилинейные отображения.

LaTeX

$$$(f : M_1 \toSL[\sigma_{12}] M_2) = g \;\Leftrightarrow\; f = g$$$

Lean4

@[simp, norm_cast]
theorem coe_inj {f g : M₁ →SL[σ₁₂] M₂} : (f : M₁ →ₛₗ[σ₁₂] M₂) = g ↔ f = g :=
  coe_injective.eq_iff

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