English
If the product of leading coefficients is nonzero, then the leading coefficient of the product equals the product of leading coefficients.
Русский
Если произведение ведущих коэффициентов не равно нулю, то ведущий коэффициент произведения равен произведению ведущих коэффициентов.
LaTeX
$$leadingCoeff (∏ i ∈ s, f i) = ∏ i ∈ s, leadingCoeff (f i)$$
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_prod` (without the `'`) for a version for integral domains,
where this condition is automatically satisfied.
-/
theorem leadingCoeff_prod' (h : (∏ i ∈ s, (f i).leadingCoeff) ≠ 0) :
(∏ i ∈ s, f i).leadingCoeff = ∏ i ∈ s, (f i).leadingCoeff := by
simpa using leadingCoeff_multiset_prod' (s.1.map f) (by simpa using h)
