English
If p ≠ 0, then (p * X^n).natTrailingDegree = p.natTrailingDegree + n.
Русский
Если p ≠ 0, то (p · X^n).natTrailingDegree = p.natTrailingDegree + n.
LaTeX
$$p \neq 0 \Rightarrow (p * X^{n}).\natTrailingDegree = p.\natTrailingDegree + n$$
Lean4
theorem natTrailingDegree_mul_X_pow {p : R[X]} (hp : p ≠ 0) (n : ℕ) :
(p * X ^ n).natTrailingDegree = p.natTrailingDegree + n :=
by
apply le_antisymm
· refine natTrailingDegree_le_of_ne_zero fun h => mt trailingCoeff_eq_zero.mp hp ?_
rwa [trailingCoeff, ← coeff_mul_X_pow]
· rw [natTrailingDegree_eq_support_min' fun h => hp (mul_X_pow_eq_zero h), Finset.le_min'_iff]
intro y hy
have key : n ≤ y := by
rw [mem_support_iff, coeff_mul_X_pow'] at hy
exact by_contra fun h => hy (if_neg h)
rw [mem_support_iff, coeff_mul_X_pow', if_pos key] at hy
exact (le_tsub_iff_right key).mp (natTrailingDegree_le_of_ne_zero hy)
