toLinearMap_injective — Mathlib

English

If the semilinear maps associated to f and g are equal, then f = g.

Русский

Если связанные с f и g полулинейные отображения равны, то f = g.

LaTeX

$$$(f : M \to_\sigma M_3) = (g : M \to_\sigma M_3) \Rightarrow f = g$$$

Lean4

theorem toLinearMap_injective {F : Type*} [FunLike F M M₃] [SemilinearMapClass F σ M M₃] {f g : F}
    (h : (f : M →ₛₗ[σ] M₃) = (g : M →ₛₗ[σ] M₃)) : f = g :=
  by
  apply DFunLike.ext
  intro m
  exact DFunLike.congr_fun h m

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