natDegree_mul_mirror — Mathlib

English

For a polynomial p over a domain R, the degree of p times its mirror is twice the degree of p.

Русский

Для полинома p над доменом R степень произведения p и зеркала p равна вдвое степени p.

LaTeX

$$$ \\operatorname{natDegree}(p \\cdot p^{\\sim}) = 2 \\operatorname{natDegree}(p) $$$

Lean4

theorem natDegree_mul_mirror : (p * p.mirror).natDegree = 2 * p.natDegree :=
  by
  by_cases hp : p = 0
  · rw [hp, zero_mul, natDegree_zero, mul_zero]
  rw [natDegree_mul hp (mt mirror_eq_zero.mp hp), mirror_natDegree, two_mul]

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