Theorems · Theorem · commutative algebra

Polynomial.exists_mul_add_mul_eq_C_resultant

∀ {m n : ℕ} {R : Type u_1} [inst : CommRing R] (f g : Polynomial R),
  f.natDegree ≤ m →
    g.natDegree ≤ n →
      m ≠ 0 ∨ n ≠ 0 → ∃ p q, p.degree < ↑n ∧ q.degree < ↑m ∧ f * p + g * q = Polynomial.C (f.resultant g m n)

Note that if n = m = 0 then resultant = 1 but f and g aren't necessarily coprime.

Defined in

Mathlib.RingTheory.Polynomial.Resultant.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRing