mul_scaleRoots' — Mathlib

English

If p and q are polynomials over a ring with no zero divisors, then (p q).scaleRoots r = p.scaleRoots r · q.scaleRoots r.

Русский

Если p и q — многочлены над кольцом без делителей нуля, то (p q).scaleRoots r = p.scaleRoots r · q.scaleRoots r.

LaTeX

$$$\text{mul_scaleRoots'}(p, q, r) : (p q).\scaleRoots r = p.\scaleRoots r \cdot q.\scaleRoots r$$$

Lean4

theorem mul_scaleRoots' (p q : R[X]) (r : R) (h : leadingCoeff p * leadingCoeff q ≠ 0) :
    (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r := by
  rw [← mul_scaleRoots, natDegree_mul' h, tsub_self, pow_zero, one_smul]

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