Commit 2025-11-29 16:10 691dd549

View on Github →

feat(RingTheory): universal coprime factorization ring (#32099)

Estimated changes

Modified Mathlib/RingTheory/Polynomial/Resultant/Basic.lean

added theorem Polynomial.isUnit_resultant_iff_isCoprime

added theorem Polynomial.resultant_eq_zero_iff

Modified Mathlib/RingTheory/Polynomial/UniversalFactorizationRing.lean

added def Polynomial.UniversalCoprimeFactorizationRing.factor₁

added theorem Polynomial.UniversalCoprimeFactorizationRing.factor₁_mul_factor₂

added def Polynomial.UniversalCoprimeFactorizationRing.factor₂

added def Polynomial.UniversalCoprimeFactorizationRing.homEquiv

added theorem Polynomial.UniversalCoprimeFactorizationRing.homEquiv_comp_fst

added theorem Polynomial.UniversalCoprimeFactorizationRing.homEquiv_comp_snd

added theorem Polynomial.UniversalCoprimeFactorizationRing.isCoprime_factor₁_factor₂

added theorem Polynomial.UniversalFactorizationRing.jacobian_resentation

added def Polynomial.UniversalFactorizationRing.presentation