reflect_add

Mathlib.Algebra.Polynomial.Reverse

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

English

Reflect is additive: reflect N (f + g) = reflect N f + reflect N g.

Русский

Reflect сохраняет сложение: reflect N (f + g) = reflect N f + reflect N g.

LaTeX

$$$\\mathrm{reflect}\\, N\\,(f+g)=\\mathrm{reflect}\\, N\\,f+\\mathrm{reflect}\\, N\\,g.$$$

Lean4

@[simp]
theorem reflect_add (f g : R[X]) (N : ℕ) : reflect N (f + g) = reflect N f + reflect N g :=
  by
  ext
  simp only [coeff_add, coeff_reflect]

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

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

Разделы

Аффилиация

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