mirror_natDegree — Mathlib

English

The natDegree of a polynomial is preserved under mirroring: p.mirror.natDegree = p.natDegree.

Русский

natDegree полинома сохраняется при зеркалировании: p.mirror.natDegree = p.natDegree.

LaTeX

$$$ p.mirror.natDegree = p.natDegree $$$

Lean4

theorem mirror_natDegree : p.mirror.natDegree = p.natDegree :=
  by
  by_cases hp : p = 0
  · rw [hp, mirror_zero]
  nontriviality R
  rw [mirror, natDegree_mul', reverse_natDegree, natDegree_X_pow,
    tsub_add_cancel_of_le p.natTrailingDegree_le_natDegree]
  rwa [leadingCoeff_X_pow, mul_one, reverse_leadingCoeff, Ne, trailingCoeff_eq_zero]

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