degree_mul — Mathlib

English

If p and q are nonzero polynomials over a semiring with no zero divisors, then deg(pq) = deg(p) + deg(q).

Русский

Если p и q не равны нулю в кольце над полем без нулевых делителей, то deg(pq) = deg(p) + deg(q).

LaTeX

$$$\deg(p q) = \deg(p) + \deg(q)$$$

Lean4

@[simp]
theorem degree_mul : degree (p * q) = degree p + degree q :=
  letI := Classical.decEq R
  if hp0 : p = 0 then by simp only [hp0, degree_zero, zero_mul, WithBot.bot_add]
  else
    if hq0 : q = 0 then by simp only [hq0, degree_zero, mul_zero, WithBot.add_bot]
    else degree_mul' <| mul_ne_zero (mt leadingCoeff_eq_zero.1 hp0) (mt leadingCoeff_eq_zero.1 hq0)

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