Theorems · Theorem · field theory

Polynomial.leadingCoeff_multiset_prod

∀ {R : Type u} [inst : CommSemiring R] [NoZeroDivisors R] (t : Multiset (Polynomial R)),
  t.prod.leadingCoeff = (Multiset.map (fun f => f.leadingCoeff) t).prod

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.

Defined in

Mathlib.Algebra.Polynomial.BigOperators

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringNoZeroDivisors