coeff_add

Mathlib.RingTheory.HahnSeries.Addition

URI: https://scilib.ai/kg/mathlib#HahnSeries.coeff_add

English

The map f respects addition: (x+y).map f = x.map f + y.map f.

Русский

Отображение f сохраняет сложение: (x+y).map f = x.map f + y.map f.

LaTeX

$$$$ ((x+y).map f) = x.map f + y.map f. $$$$

Lean4

theorem coeff_add {x y : HahnSeries Γ R} {a : Γ} : (x + y).coeff a = x.coeff a + y.coeff a :=
  rfl

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

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

Разделы

Аффилиация

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