English
The leading coefficient of a product of polynomials equals the product of leading coefficients provided the product of leading coefficients is nonzero.
Русский
Ведущий коэффициент произведения полиномов равен произведению ведущих коэффициентов при условии, что произведение ведущих коэффициентов не равно нулю.
LaTeX
$$leadingCoeff (t.prod) = (t.map leadingCoeff).prod$$
Lean4
/-- The leading coefficient of a product of polynomials is equal to
the product of the leading coefficients, provided that this product is nonzero.
See `Polynomial.leadingCoeff_multiset_prod` (without the `'`) for a version for integral domains,
where this condition is automatically satisfied.
-/
theorem leadingCoeff_multiset_prod' (h : (t.map leadingCoeff).prod ≠ 0) :
t.prod.leadingCoeff = (t.map leadingCoeff).prod :=
by
induction t using Multiset.induction_on with
| empty => simp
| cons a t ih => ?_
simp only [Multiset.map_cons, Multiset.prod_cons] at h ⊢
rw [Polynomial.leadingCoeff_mul']
· rw [ih]
simp only [ne_eq]
apply right_ne_zero_of_mul h
· rw [ih]
· exact h
simp only [ne_eq]
apply right_ne_zero_of_mul h
