subst_smul — Mathlib

English

Substitution commutes with scalar multiplication: subst a (r • f) = r • (subst a f).

Русский

Подстановка коммутирует с умножением на скаляр: subst a (r • f) = r • (subst a f).

LaTeX

$$$\\operatorname{subst}\\ a\\ (r \\cdot f) = r \\cdot (\\operatorname{subst}\\ a\\ f)$$$

Lean4

theorem subst_smul (ha : HasSubst a) (r : A) (f : MvPowerSeries σ R) : subst a (r • f) = r • (subst a f) := by
  simp only [← substAlgHom_apply ha, AlgHom.map_smul_of_tower]

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