dvd_cancelLeads_of_dvd_of_dvd — Mathlib

English

Under mild commutativity assumptions, the same degree bound holds for natDegree(p.cancelLeads q) as above when p.natDegree ≤ q.natDegree and 0 < q.natDegree.

Русский

При условии некоторого коммутирования, аналогичное ограничение по степени справедливо и в общем случае natDegree(p.cancelLeads q) < q.natDegree.

LaTeX

$$$p.natDegree \\le q.natDegree \\land 0 < q.natDegree \\Rightarrow (p.cancelLeads q).natDegree < q.natDegree$$$

Lean4

theorem dvd_cancelLeads_of_dvd_of_dvd {r : R[X]} (pq : p ∣ q) (pr : p ∣ r) : p ∣ q.cancelLeads r :=
  dvd_sub (pr.trans (Dvd.intro_left _ rfl)) (pq.trans (Dvd.intro_left _ rfl))

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