English
For a nonzero coefficient x and natural n, the coefficient list of monomial n with coeff x equals x followed by n zeros.
Русский
Для ненулевого коэффициента x и натурального n, коэффициентный список монома n x равен x далее n нулей.
LaTeX
$$$ (\\text{monomial } n\\ x).coeffList = x :: \\text{List.replicate } n 0 $ при x ≠ 0$$
Lean4
@[simp]
theorem coeffList_monomial {x : R} (hx : x ≠ 0) (n : ℕ) : (monomial n x).coeffList = x :: List.replicate n 0 :=
by
have h := mt (Polynomial.monomial_eq_zero_iff x n).mp hx
apply List.ext_get (by classical simp [hx])
rintro (_ | k) _ h₁
· exact (coeffList_eq_cons_leadingCoeff h).rec (by simp_all)
· rw [List.length_cons, List.length_replicate] at h₁
have : ((monomial n) x).natDegree.succ = n + 1 := by simp [Polynomial.natDegree_monomial_eq n hx]
simpa [coeffList, withBotSucc_degree_eq_natDegree_add_one h] using
Polynomial.coeff_monomial_of_ne _
(by cutsat)
/- Coefficients of a polynomial `P` are always the leading coefficient, some number of zeros, and
then `coeffList P.eraseLead`. -/
