degree_le_of_dvd — Mathlib

English

For p, q with no zero divisors, (p · q).natDegree = p.natDegree + q.natDegree.

Русский

Для p, q над кольцом без нулевых делителей, (p · q).natDegree = p.natDegree + q.natDegree.

LaTeX

$$(p ≠ 0) → (q ≠ 0) → (p q).natDegree = p.natDegree + q.natDegree$$

Lean4

theorem degree_le_of_dvd (h1 : p ∣ q) (h2 : q ≠ 0) : degree p ≤ degree q :=
  by
  rcases h1 with ⟨q, rfl⟩; rw [mul_ne_zero_iff] at h2
  exact degree_le_mul_left p h2.2

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