English
For a finite set s, the leading coefficient of the product ∏_{i∈s} f_i equals the product of the leading coefficients: leadingCoeff(∏ f_i) = ∏ leadingCoeff(f_i).
Русский
Для конечного множества s ведущий коэффициент произведения равен произведению ведущих коэффициентов.
LaTeX
$$$$\operatorname{leadingCoeff}\left( \prod_{i\in s} f_i \right) = \prod_{i\in s} \operatorname{leadingCoeff}(f_i).$$$$
Lean4
/-- The leading coefficient of a product of polynomials is equal to
the product of the leading coefficients.
See `Polynomial.leadingCoeff_prod'` (with a `'`) for a version for commutative semirings,
where additionally, the product of the leading coefficients must be nonzero.
-/
theorem leadingCoeff_prod : (∏ i ∈ s, f i).leadingCoeff = ∏ i ∈ s, (f i).leadingCoeff := by
simpa using leadingCoeff_multiset_prod (s.1.map f)
