coe_add

Mathlib.RingTheory.PowerSeries.Basic

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

English

The embedding commutes with addition: ((φ + ψ : R[X]) : PowerSeries R) = φ + ψ.

Русский

Вложение сохраняет суммацию: ((φ + ψ : R[X]) : PowerSeries R) = φ + ψ.

LaTeX

$$$((\\varphi + \\psi : R[X]) : PowerSeries R) = \\varphi + \\psi$$$

Lean4

@[simp, norm_cast]
theorem coe_add : ((φ + ψ : R[X]) : PowerSeries R) = φ + ψ :=
  by
  ext
  simp

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

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

Разделы

Аффилиация

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