coeff_apply_le — Mathlib

English

If natDegree f ≤ i, then h.coeff z i = 0.

Русский

Если natDegree f ≤ i, то h.coeff z i = 0.

LaTeX

$$$ h.coeff\\, z\\, i = 0$ при $\\operatorname{natDegree} f \\le i$$$

Lean4

theorem coeff_apply_le (z : S) (i : ℕ) (hi : natDegree f ≤ i) : h.coeff z i = 0 :=
  by
  simp only [coeff, liftPolyₗ_apply, LinearMap.coe_mk, AddHom.coe_mk]
  nontriviality R
  exact
    Polynomial.coeff_eq_zero_of_degree_lt
      ((degree_modByMonic_lt _ h.monic).trans_le (Polynomial.degree_le_of_natDegree_le hi))

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