Theorems · Definition · commutative algebra

Polynomial.UniversalFactorizationRing.presentation

{R : Type u_1} →
  [inst : CommRing R] →
    {n : ℕ} →
      (m k : ℕ) →
        (hn : n = m + k) →
          (p : Polynomial.MonicDegreeEq R n) →
            Algebra.PreSubmersivePresentation R (Polynomial.UniversalFactorizationRing m k hn p) (Fin m ⊕ Fin k) (Fin n)

The presentation of UniversalFactorizationRing. Its jacobian is the resultant of the two factors (up to sign).

Defined in

Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Cited by

6 results in Mathlib

Foundations

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

Assumes

CommRing