not_dvd_of_natDegree_lt — Mathlib

English

If p is monic, q ≠ 0, and degree q < degree p, then p does not divide q.

Русский

Если p моноическое, q ≠ 0 и deg q < deg p, то p не делится на q.

LaTeX

$$$Monic(p) \land q \neq 0 \land \deg q < \deg p \Rightarrow p \nmid q$$$

Lean4

theorem not_dvd_of_natDegree_lt (hp : Monic p) (h0 : q ≠ 0) (hl : natDegree q < natDegree p) : ¬p ∣ q :=
  by
  rintro ⟨r, rfl⟩
  rw [hp.natDegree_mul' <| right_ne_zero_of_mul h0] at hl
  exact hl.not_ge (Nat.le_add_right _ _)

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