homogenize_sub

Mathlib.Algebra.Polynomial.Homogenize

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

English

For polynomials p,q ∈ R[X], (p − q).homogenize n = p.homogenize n − q.homogenize n.

Русский

Для многочленов p,q ∈ R[X] имеет место (p − q).homogenize n = p.homogenize n − q.homogenize n.

LaTeX

$$$ (p - q)^{\\mathrm{hom}}_n = p^{\\mathrm{hom}}_n - q^{\\mathrm{hom}}_n. $$$

Lean4

@[simp]
theorem homogenize_sub (p q : R[X]) (n : ℕ) : (p - q).homogenize n = p.homogenize n - q.homogenize n :=
  map_sub (homogenizeLM n) p q

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

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

Разделы

Аффилиация

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