English
For any f ∈ R[X], natDegree(f) = natDegree(reverse f) + natTrailingDegree(f). In particular, this holds with zero-trailing cases.
Русский
Для любого f ∈ R[X] natDegree(f) = natDegree(reverse f) + natTrailingDegree(f) (при нулевом полиноме обе стороны равны нулю).
LaTeX
$$$\operatorname{natDegree}(f) = \operatorname{natDegree}(\operatorname{reverse}(f)) + \operatorname{natTrailingDegree}(f).$$$
Lean4
theorem natDegree_eq_reverse_natDegree_add_natTrailingDegree (f : R[X]) :
f.natDegree = f.reverse.natDegree + f.natTrailingDegree :=
by
by_cases hf : f = 0
· rw [hf, reverse_zero, natDegree_zero, natTrailingDegree_zero]
apply le_antisymm
· refine tsub_le_iff_right.mp ?_
apply le_natDegree_of_ne_zero
rw [reverse, coeff_reflect, ← revAt_le f.natTrailingDegree_le_natDegree, revAt_invol]
exact trailingCoeff_nonzero_iff_nonzero.mpr hf
· rw [← le_tsub_iff_left f.reverse_natDegree_le]
apply natTrailingDegree_le_of_ne_zero
have key := mt leadingCoeff_eq_zero.mp (mt reverse_eq_zero.mp hf)
rwa [leadingCoeff, coeff_reverse, revAt_le f.reverse_natDegree_le] at key
