natDegree_mul — Mathlib

English

If p ≠ 0 and q ≠ 0, then (p q).natDegree = p.natDegree + q.natDegree.

Русский

Если p ≠ 0 и q ≠ 0, то (p q).natDegree = p.natDegree + q.natDegree.

LaTeX

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

Lean4

theorem natDegree_mul (hp : p ≠ 0) (hq : q ≠ 0) : (p * q).natDegree = p.natDegree + q.natDegree := by
  rw [← Nat.cast_inj (R := WithBot ℕ), ← degree_eq_natDegree (mul_ne_zero hp hq), Nat.cast_add, ←
    degree_eq_natDegree hp, ← degree_eq_natDegree hq, degree_mul]

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