Theorems · Theorem · commutative algebra

MvPolynomial.universalFactorizationMapPresentation_jacobiMatrix

∀ (R : Type u_1) [inst : CommRing R] (n m k : ℕ) (hn : n = m + k),
  (MvPolynomial.universalFactorizationMapPresentation R n m k hn).jacobiMatrix =
    -((Matrix.reindex (finCongr ⋯) (finCongr ⋯))
          ((Polynomial.map
                ((MvPolynomial.mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))).comp
                    (MvPolynomial.rename Sum.inl)).toRingHom
                (Polynomial.freeMonic R m)).sylvester
            (Polynomial.map
              ((MvPolynomial.mapAlgHom (Algebra.ofId R (MvPolynomial (Fin n) R))).comp
                  (MvPolynomial.rename Sum.inr)).toRingHom
              (Polynomial.freeMonic R k))
            m k)).transpose

Defined in

Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRing