Theorems · Theorem · commutative algebra

Polynomial.resultant_eq_prod_roots_sub

∀ {K : Type u_3} [inst : Field K] (f g : Polynomial K),
  f.Monic →
    g.Monic → f.Splits → g.Splits → f.resultant g = (Multiset.map (fun ij => ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod

If f and g are monic and splits, then Res(f, g) = ∏ (α - β), where α and β runs through the roots of f and g respectively.

Defined in

Mathlib.RingTheory.Polynomial.Resultant.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

Field