subst_mul — Mathlib

English

Substitution respects multiplication: subst a (f g) = subst a f · subst a g.

Русский

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

LaTeX

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

Lean4

theorem subst_mul (ha : HasSubst a) (f g : MvPowerSeries σ R) : subst a (f * g) = subst a f * subst a g := by
  simp only [← substAlgHom_apply ha, map_mul]

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