natTrailingDegree_mul_mirror — Mathlib

English

For a polynomial p over a semiring R with no zero divisors, the trailing-degree of p·p̃ is twice the trailing-degree of p.

Русский

Для полинома p над полусемирингом R без нулевых делителей трекинг посл. степени выполняется: natTrailingDegree(p·p̃) = 2·natTrailingDegree(p).

LaTeX

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

Lean4

theorem natTrailingDegree_mul_mirror : (p * p.mirror).natTrailingDegree = 2 * p.natTrailingDegree :=
  by
  by_cases hp : p = 0
  · rw [hp, zero_mul, natTrailingDegree_zero, mul_zero]
  rw [natTrailingDegree_mul hp (mt mirror_eq_zero.mp hp), mirror_natTrailingDegree, two_mul]

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