English
Under the same multiplicativity, (p q).scaleRoots r = p.scaleRoots r · q.scaleRoots r when leading coeffs are nonzero.
Русский
При тех же условиях неотрицательных ведущих коэффициентов: (p q).scaleRoots r = p.scaleRoots r · q.scaleRoots r, если ведущие коэффициенты не нулевые.
LaTeX
$$$ (p q).\scaleRoots r = p.\scaleRoots r \cdot q.\scaleRoots r $ under suitable nonzero-leading-coefficient assumptions.$$
Lean4
/-- 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'`. -/
theorem mul_scaleRoots (p q : R[X]) (r : R) :
r ^ (natDegree p + natDegree q - natDegree (p * q)) • (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r :=
by
ext n; simp only [coeff_scaleRoots, coeff_smul, smul_eq_mul]
trans (∑ x ∈ Finset.antidiagonal n, coeff p x.1 * coeff q x.2) * r ^ (natDegree p + natDegree q - n)
· rw [← coeff_mul]
cases lt_or_ge (natDegree (p * q)) n with
| inl h => simp only [coeff_eq_zero_of_natDegree_lt h, zero_mul, mul_zero]
| inr h => rw [mul_comm, mul_assoc, ← pow_add, add_comm, tsub_add_tsub_cancel natDegree_mul_le h]
· rw [coeff_mul, Finset.sum_mul]
apply Finset.sum_congr rfl
simp only [Finset.mem_antidiagonal, coeff_scaleRoots, Prod.forall]
intro a b e
cases lt_or_ge (natDegree p) a with
| inl h => simp only [coeff_eq_zero_of_natDegree_lt h, zero_mul]
| inr ha =>
cases lt_or_ge (natDegree q) b with
| inl h => simp only [coeff_eq_zero_of_natDegree_lt h, zero_mul, mul_zero]
| inr hb =>
simp only [← e, mul_assoc, mul_comm (r ^ (_ - a)), ← pow_add]
rw [add_comm (_ - _), tsub_add_tsub_comm ha hb]
