add

Mathlib.RingTheory.PolynomialLaw.Basic

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

English

The sum of two polynomial laws is again a polynomial law.

Русский

Сумма двух полиномальных законов опять является полиномальным законом.

LaTeX

$$$f,g: M \to_p_l[R] N \;\Rightarrow\; f+g \in \operatorname{PolyLaw}(R,M,N).$$$

Lean4

/-- The sum of two polynomial laws -/
noncomputable def add : M →ₚₗ[R] N where toFun' S _ _ := f.toFun' S + g.toFun' S

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

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

Разделы

Аффилиация

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