degree_mul — Mathlib

English

If the product of leading coefficients is nonzero, then natDegree(p q) = natDegree p + natDegree q.

Русский

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

LaTeX

$$natDegree(p q) = natDegree(p) + natDegree(q) при leadingCoeff p * leadingCoeff q ≠ 0$$

Lean4

theorem degree_mul (hq : Monic q) : degree (p * q) = degree p + degree q :=
  letI := Classical.decEq R
  if hp : p = 0 then by simp [hp] else degree_mul' <| by rwa [hq.leadingCoeff, mul_one, Ne, leadingCoeff_eq_zero]

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