Theorems · Theorem · commutative algebra

Polynomial.resultant_eq_prod_eval

∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] (f g : Polynomial R) (n : ℕ),
  g.natDegree ≤ n →
    f.Splits →
      f.resultant g f.natDegree n = f.leadingCoeff ^ n * (Multiset.map (fun x => Polynomial.eval x g) f.roots).prod

If f splits with leading coeff a and degree n, then Res(f, g) = aⁿ * ∏ g(α) where α runs through the roots of f.

Defined in

Mathlib.RingTheory.Polynomial.Resultant.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingIsDomain