Theorems · Theorem · commutative algebra

Polynomial.mul_scaleRoots

∀ {R : Type u_1} [inst : CommSemiring R] (p q : Polynomial R) (r : R),
  r ^ (p.natDegree + q.natDegree - (p * q).natDegree) • (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r

Multiplication and scaleRoots commute up to a power of r. The factor disappears if we assume that the product of the leading coeffs does not vanish. See Polynomial.mul_scaleRoots'.

Defined in

Mathlib.RingTheory.Polynomial.ScaleRoots

Cited by

2 results in Mathlib

Foundations

Depth 105 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiring