le_natTrailingDegree — Mathlib

English

If p ≠ 0 and p.coeff(m) = 0 for all m < n, then n ≤ natTrailingDegree(p).

Русский

Если p ≠ 0 и p.coeff(m) = 0 для всех m < n, то n ≤ natTrailingDegree(p).

LaTeX

$$p \neq 0 \land (\forall m < n, p.\coeff(m) = 0) \Rightarrow n \le \operatorname{natTrailingDegree}(p)$$

Lean4

theorem le_natTrailingDegree (hp : p ≠ 0) (hn : ∀ m < n, p.coeff m = 0) : n ≤ p.natTrailingDegree :=
  by
  rw [natTrailingDegree_eq_support_min' hp]
  exact Finset.le_min' _ _ _ fun m hm => not_lt.1 fun hmn => mem_support_iff.1 hm <| hn _ hmn

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