coe_add

Mathlib.Algebra.MonoidAlgebra.Defs

URI: https://scilib.ai/kg/mathlib#MonoidAlgebra.coe_add

English

The coercion to functions is additive: (f+g) coerces to the sum of their pointwise values.

Русский

Коэрция к функциям сохраняет сложение: отображение f+g даёт точечно f+g.

LaTeX

$$$\\mathrm{coe}_{MonoidAlgebra}(f+g) = \\mathrm{coe}_{MonoidAlgebra}(f) + \\mathrm{coe}_{MonoidAlgebra}(g)$$$

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem coe_add (f g : MonoidAlgebra R G) : ⇑(f + g) = f + g :=
  rfl

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

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

Разделы

Аффилиация

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