smul — Mathlib

English

If a linear map g agrees with f' on all simple tensors, then g equals lift f'.

Русский

Если линейное отображение g совпадает с f' на всех простых тензорах, то g равно lift f'.

LaTeX

$$$\\forall g : M \\otimes_R N \\to_+ P_2, \\; (\\forall x,y, g(x ⊗ y) = f' x y) \\Rightarrow g = \\mathrm{lift}\, f'.$$$

Lean4

theorem smul (r : R) (x) : liftAux f (r • x) = r • liftAux f x :=
  liftAux.smulₛₗ _ _

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