eq_zero_of_dvd_of_natDegree_lt — Mathlib

English

Let R be a semiring with no zero divisors. If p and q are polynomials in R[X], and p divides q while the natural degree of q is strictly less than the natural degree of p, then q must be the zero polynomial.

Русский

Пусть R — полугруппа без делителей нуля. Пусть p, q ∈ R[X]. Если p делит q и natDegree(q) < natDegree(p), тогда q равно нулю.

LaTeX

$$$\\\\forall R [\\\\text{Semiring } R] [\\\\text{NoZeroDivisors } R], \\\\forall p,q \in R[X], \\\\bigl(p \\mid q \\land \\\\operatorname{natDegree}(q) < \\\\operatorname{natDegree}(p)\\\\bigr) \Rightarrow q = 0$$$

Lean4

theorem eq_zero_of_dvd_of_natDegree_lt (h₁ : p ∣ q) (h₂ : natDegree q < natDegree p) : q = 0 :=
  by
  by_contra hc
  exact lt_iff_not_ge.mp h₂ (natDegree_le_of_dvd h₁ hc)

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