Theorems · Definition · commutative algebra
Polynomial.UniversalCoprimeFactorizationRing
{R : Type u_1} → [inst : CommRing R] → {n : ℕ} → (m k : ℕ) → n = m + k → Polynomial.MonicDegreeEq R n → Type u_1The universal coprime factorization ring of a monic polynomial p of degree n.
This is the representing object of the functor
S ↦ "factorizations of p into coprime (monic deg m) * (monic deg k) in S".
See UniversalCoprimeFactorizationRing.homEquiv.
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 128 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- Localization.Awayproof · cited by 162
- Algebra.PreSubmersivePresentation.jacobianproof · cited by 31
- Polynomial.MonicDegreeEqstatement and proof · cited by 22
- Polynomial.UniversalFactorizationRing.presentationproof · cited by 6
Cited by10
Results whose statement or proof uses this declaration.
- Polynomial.UniversalCoprimeFactorizationRing.factor₁statement and proof · cited by 4
- Polynomial.UniversalCoprimeFactorizationRing.factor₂statement and proof · cited by 4
- Polynomial.UniversalCoprimeFactorizationRing.homEquivstatement and proof · cited by 3
- Polynomial.UniversalCoprimeFactorizationRing.exists_liesOver_residueFieldMap_bijectivestatement and proof · cited by 1
- Polynomial.UniversalCoprimeFactorizationRing.factor₁_mul_factor₂statement and proof · cited by 1
- Polynomial.UniversalCoprimeFactorizationRing.homEquiv_comp_fststatement and proof · cited by 1
- Polynomial.UniversalCoprimeFactorizationRing.homEquiv_comp_sndstatement and proof · cited by 1
- Polynomial.UniversalCoprimeFactorizationRing.isCoprime_factor₁_factor₂statement and proof · cited by 1
- Polynomial.UniversalCoprimeFactorizationRing.congr_simpstatement and proof · cited by 0