2026-01-06 11:03
Mathlib/RingTheory/Polynomial/UniversalFactorizationRing.lean
feat(RingTheory): construct etale neighborhood that isolates point in fiber (#32823)
Added Polynomial.UniversalCoprimeFactorizationRing.exists_liesOver_residueFieldMap_bijective