Theorems · Definition · commutative algebra

Polynomial.UniversalFactorizationRing

{R : Type u_1} → [inst : CommRing R] → {n : ℕ} → (m k : ℕ) → n = m + k → Polynomial.MonicDegreeEq R n → Type u_1

The universal factorization ring of a monic polynomial p of degree n. This is the representing object of the functor S ↦ "factorizations of p into (monic deg m) * (monic deg k) in S". See UniversalFactorizationRing.homEquiv.

Defined in

Mathlib.RingTheory.Polynomial.UniversalFactorizationRing

Cited by

10 results in Mathlib

Foundations

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

Assumes

CommRing