map_smul — Mathlib

English

The induced map from quotientPiLift respects scalar multiplication: L(r • x) = r • L(x).

Русский

Отображение сохраняет умножение на скаляр: L(r·x) = r·L(x).

LaTeX

$$LinearMap.map_smul (quotientPiLift ...) r x$$

Lean4

theorem map_smul (r : R) (x : ((i : ι) → Ms i) ⧸ pi Set.univ p) : toFun p (r • x) = (RingHom.id R r) • toFun p x :=
  LinearMap.map_smul (quotientPiLift p (fun i => (p i).mkQ) fun i => (ker_mkQ (p i)).ge) r x

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