map_smul — Mathlib

English

The only vector that maps to zero under e is the zero vector: for all x, e(x) = 0 iff x = 0.

Русский

Единственный вектор, который отображается в нуль, это нуль: для всех x верно e(x) = 0 ⇔ x = 0.

LaTeX

$$$\forall x\,(e(x) = 0 \iff x = 0)$$$

Lean4

theorem map_smul [Module R₁ M₂] (e : M₁ ≃L[R₁] M₂) (c : R₁) (x : M₁) : e (c • x) = c • e x :=
  (e : M₁ →L[R₁] M₂).map_smul c x

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