Root scaling of finite products

Scaling roots commutes with finite products over a commutative semiring without zero divisors, and with finite products of monic polynomials over any commutative semiring. This transports factorizations into linear factors through integral normalization. Scaling the roots by s also multiplies the subleading coefficient by s, so it preserves the vanishing of that coefficient.

@[simp]

theorem Polynomial.nextCoeff_scaleRoots {R : Type u_1} [CommSemiring R] (p : Polynomial R) (s : R) : (p.scaleRoots s).nextCoeff = p.nextCoeff * s

Scaling the roots by s multiplies the subleading coefficient by s.

theorem Polynomial.prod_scaleRoots_of_monic {R : Type u_1} {ι : Type u_2} [CommSemiring R] (s : Finset ι) (f : ι → Polynomial R) (a : R) (hf : ∀ i ∈ s, (f i).Monic) : (∏ i ∈ s, f i).scaleRoots a = ∏ i ∈ s, (f i).scaleRoots a

Scaling roots commutes with a finite product of monic polynomials, even when the coefficient semiring has zero divisors.

@[simp]

theorem Polynomial.prod_scaleRoots {R : Type u_1} {ι : Type u_2} [CommSemiring R] [NoZeroDivisors R] (s : Finset ι) (f : ι → Polynomial R) (a : R) : (∏ i ∈ s, f i).scaleRoots a = ∏ i ∈ s, (f i).scaleRoots a

Scaling all roots of a finite product scales the roots of every factor.