not_dvd_of_degree_lt — Mathlib

English

Not divides by degree condition equivalent formulation: Monic p, q ≠ 0, degree q < degree p implies p ∤ 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_degree_lt (hp : Monic p) (h0 : q ≠ 0) (hl : degree q < degree p) : ¬p ∣ q :=
  Monic.not_dvd_of_natDegree_lt hp h0 <| natDegree_lt_natDegree h0 hl

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