not_dvd_of_degree_lt — Mathlib

English

Let R be a semiring with no zero divisors. If q is a nonzero polynomial and its degree is strictly less than the degree of p, then p does not divide q.

Русский

Пусть R — полугруппа без делителей нуля. Если q ≠ 0 и deg(q) < deg(p), тогда p не делит q.

LaTeX

$$$\\\\forall R [\\\\text{Semiring } R] [\\\\text{NoZeroDivisors } R], \\\\forall p,q \\in R[X], q \\\\neq 0 \\\\land \\\\operatorname{deg}(q) < \\\\operatorname{deg}(p) \\\\Rightarrow \\\\neg (p \\mid q)$$$

Lean4

theorem not_dvd_of_degree_lt (h0 : q ≠ 0) (hl : q.degree < p.degree) : ¬p ∣ q :=
  by
  by_contra hcontra
  exact h0 (eq_zero_of_dvd_of_degree_lt hcontra hl)

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