subst_add — Mathlib

English

Substitution distributes over addition: substituting into a sum equals the sum of substitutions.

Русский

Подстановка распределяется по сложению: подстановка в сумму равна сумме подстановок.

LaTeX

$$$\forall ha\, (f,g : PowerSeries R),\ subst a (f+g) = subst a f + subst a g$$$

Lean4

theorem subst_add (ha : HasSubst a) (f g : PowerSeries R) : subst a (f + g) = subst a f + subst a g := by
  rw [← coe_substAlgHom ha, map_add]

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