Theorems · Theorem · commutative algebra

Polynomial.toMatrix_sylvesterMap

∀ {m n : ℕ} {R : Type u_1} [inst : CommRing R] (f g : Polynomial R) (hf : f.natDegree ≤ m) (hg : g.natDegree ≤ n),
  (LinearMap.toMatrix ((Polynomial.degreeLT.basis R m).prod (Polynomial.degreeLT.basis R n))
        (Polynomial.degreeLT.basis R (m + n)))
      (f.sylvesterMap g hf hg) =
    (Matrix.reindex (Equiv.refl (Fin (m + n))) finSumFinEquiv.symm) (f.sylvester g m n)

Defined in

Mathlib.RingTheory.Polynomial.Resultant.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRing