coe_add — Mathlib

English

Let f and g be polynomials. The evaluation map is additive: for every a ∈ α, (f + g)(a) = f(a) + g(a). Equivalently, the function associated to f + g is the sum of the functions associated to f and g.

Русский

Пусть f и g — полиномы над α. Отображение, сопоставляющее полиномам функции, сохраняет сложение: для любого a ∈ α выполняется (f + g)(a) = f(a) + g(a). Эквивалентно, функция, соответствующая f + g, есть сумма функций f и g.

LaTeX

$$$$ \\widehat{f+g} = \\widehat{f} + \\widehat{g} $$$$

Lean4

@[simp]
theorem coe_add (f g : Poly α) : ⇑(f + g) = f + g :=
  rfl

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