English
The coefficient of p^n at degree n times natDegree(p) equals the nth power of the leading coefficient of p.
Русский
Коэффициент (p^n) на степени n · natDegree(p) равен (leadingCoeff(p))^n.
LaTeX
$$$ (p^n).coeff (n \cdot p.natDegree) = (p.leadingCoeff)^n. $$$
Lean4
@[simp]
theorem coeff_pow_mul_natDegree (p : R[X]) (n : ℕ) : (p ^ n).coeff (n * p.natDegree) = p.leadingCoeff ^ n := by
induction n with
| zero => simp
| succ i hi =>
rw [pow_succ, pow_succ, Nat.succ_mul]
by_cases hp1 : p.leadingCoeff ^ i = 0
· rw [hp1, zero_mul]
by_cases hp2 : p ^ i = 0
· rw [hp2, zero_mul, coeff_zero]
· apply coeff_eq_zero_of_natDegree_lt
have h1 : (p ^ i).natDegree < i * p.natDegree :=
by
refine lt_of_le_of_ne natDegree_pow_le fun h => hp2 ?_
rw [← h, hp1] at hi
exact leadingCoeff_eq_zero.mp hi
calc
(p ^ i * p).natDegree ≤ (p ^ i).natDegree + p.natDegree := natDegree_mul_le
_ < i * p.natDegree + p.natDegree := add_lt_add_right h1 _
· rw [← natDegree_pow' hp1, ← leadingCoeff_pow' hp1]
exact coeff_mul_degree_add_degree _ _
