nextCoeff_mul — Mathlib

English

If p and q are monic, then nextCoeff(p q) = nextCoeff(p) + nextCoeff(q).

Русский

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

LaTeX

$$$Monic(p) \land Monic(q) \Rightarrow \text{nextCoeff}(p q) = \text{nextCoeff}(p) + \text{nextCoeff}(q)$$$

Lean4

theorem nextCoeff_mul (hp : Monic p) (hq : Monic q) : nextCoeff (p * q) = nextCoeff p + nextCoeff q :=
  by
  nontriviality
  simp only [← coeff_one_reverse]
  rw [reverse_mul] <;> simp [hp.leadingCoeff, hq.leadingCoeff, mul_coeff_one, add_comm]

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