add

Mathlib.RingTheory.PowerSeries.Substitution

URI: https://scilib.ai/kg/mathlib#PowerSeries.HasSubst.add

English

If f and g admit substitution, then their sum f+g also admits substitution.

Русский

Если у f и g есть подстановка, то и сумма f+g имеет подстановку.

LaTeX

$$$\forall f,g:\ PowerSeries\ R,\ HasSubst f \to HasSubst g \to HasSubst\bigl(f+g\bigr)$$$

Lean4

theorem add (hf : HasSubst f) (hg : HasSubst g) : HasSubst (f + g) :=
  (Commute.all _ _).isNilpotent_add hf hg

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru