Theorems · Theorem · field theory

Polynomial.leadingCoeff_prod

∀ {R : Type u} {ι : Type w} (s : Finset ι) [inst : CommSemiring R] [NoZeroDivisors R] (f : ι → Polynomial R),
  (∏ i ∈ s, f i).leadingCoeff = ∏ i ∈ s, (f i).leadingCoeff

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.

Defined in

Mathlib.Algebra.Polynomial.BigOperators

Cited by

0 results in Mathlib

Foundations

Depth 114 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringNoZeroDivisors