isLinearMap_of_compatibleSMul — Mathlib

English

If two σ-linear maps are equal on 1, then they are equal overall.

Русский

Если две σ-линейные отображения совпадают на единице, то они совпадают во всём.

LaTeX

$$$ f = g \quad \text{если } f(1) = g(1) $$$

Lean4

theorem isLinearMap_of_compatibleSMul [Module S M] [Module S M₂] [CompatibleSMul M M₂ R S] (f : M →ₗ[S] M₂) :
    IsLinearMap R f where
  map_add := map_add f
  map_smul := map_smul_of_tower f

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