natDegree_mul' — Mathlib

English

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

Русский

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

LaTeX

$$$Monic(p) \land q \neq 0 \land \operatorname{natDegree}(q) < \operatorname{natDegree}(p) \Rightarrow p \nmid q$$$

Lean4

nonrec theorem natDegree_mul' (hp : p.Monic) (hq : q ≠ 0) : (p * q).natDegree = p.natDegree + q.natDegree :=
  by
  rw [natDegree_mul']
  simpa [hp.leadingCoeff, leadingCoeff_ne_zero]

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