English
The leading coefficient of a product of polynomials equals the product of their leading coefficients: leadingCoeff(∏ t) = ∏ leadingCoeff(p) for p ∈ t.
Русский
Ведущий коэффициент произведения многочленов равен произведению их ведущих коэффициентов.
LaTeX
$$$$\operatorname{leadingCoeff}\left( t.prod \right) = \prod_{p\in t} \operatorname{leadingCoeff}(p).$$$$
Lean4
/-- The leading coefficient of a product of polynomials is equal to
the product of the leading coefficients.
See `Polynomial.leadingCoeff_multiset_prod'` (with a `'`) for a version for commutative semirings,
where additionally, the product of the leading coefficients must be nonzero.
-/
theorem leadingCoeff_multiset_prod : t.prod.leadingCoeff = (t.map fun f => leadingCoeff f).prod :=
by
rw [← leadingCoeffHom_apply, MonoidHom.map_multiset_prod]
simp only [leadingCoeffHom_apply]
