degree_lt_iff_coeff_zero — Mathlib

English

degree f < n iff coeff f m = 0 for all m ≥ n.

Русский

degree f < n тогда и только тогда, когда coeff f m = 0 для всех m ≥ n.

LaTeX

$$degree(f) < n ↔ ∀ m, n ≤ m → coeff(f, m) = 0$$

Lean4

theorem degree_lt_iff_coeff_zero (f : R[X]) (n : ℕ) : degree f < n ↔ ∀ m : ℕ, n ≤ m → coeff f m = 0 := by
  simp only [degree, Finset.sup_lt_iff (WithBot.bot_lt_coe n), mem_support_iff, WithBot.coe_lt_coe, ← @not_le ℕ,
    max_eq_sup_coe, Nat.cast_withBot, Ne, not_imp_not]

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