add_def

Mathlib.RingTheory.PolynomialLaw.Basic

URI: https://scilib.ai/kg/mathlib#PolynomialLaw.add_def

English

The evaluation of the sum at S equals the sum of evaluations at S: (f+g).toFun' S = f.toFun' S + g.toFun' S.

Русский

Значение суммы в S равно сумме значений: (f+g).toFun' S = f.toFun' S + g.toFun' S.

LaTeX

$$$(f+g)^{\mathrm{toFun}'}_S = f^{\mathrm{toFun}'}_S + g^{\mathrm{toFun}'}_S$$$

Lean4

@[simp]
theorem add_def (S : Type u) [CommSemiring S] [Algebra R S] : (f + g).toFun' S = f.toFun' S + g.toFun' S :=
  rfl

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

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

Разделы

Аффилиация

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