reverse_natDegree — Mathlib

English

For any f ∈ R[X], reverse f has natDegree equal to natDegree(f) minus natTrailingDegree(f): reverse(f).natDegree = f.natDegree − f.natTrailingDegree.

Русский

Для любого f ∈ R[X] natDegree(reverse f) = natDegree(f) − natTrailingDegree(f).

LaTeX

$$$\operatorname{natDegree}(\operatorname{reverse}(f)) = \operatorname{natDegree}(f) - \operatorname{natTrailingDegree}(f).$$$

Lean4

theorem reverse_natDegree (f : R[X]) : f.reverse.natDegree = f.natDegree - f.natTrailingDegree := by
  rw [f.natDegree_eq_reverse_natDegree_add_natTrailingDegree, add_tsub_cancel_right]

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