natDegree_mul_comm — Mathlib

English

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

Русский

Если p моноическое, q ≠ 0, то natDegree(p q) = natDegree(p) + natDegree(q).

LaTeX

$$$Monic(p) \land q \neq 0 \Rightarrow \operatorname{natDegree}(p q) = \operatorname{natDegree}(p) + \operatorname{natDegree}(q)$$$

Lean4

theorem natDegree_mul_comm (hp : p.Monic) (q : R[X]) : (p * q).natDegree = (q * p).natDegree :=
  by
  by_cases h : q = 0
  · simp [h]
  rw [hp.natDegree_mul' h, Polynomial.natDegree_mul', add_comm]
  simpa [hp.leadingCoeff, leadingCoeff_ne_zero]

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