Mathlib Changelog
v4
Changelog
About
Github
Theorem
Algebra.exists_etale_bijective_residueFieldMap_and_map_eq_mul_and_isCoprime.{u}
Modification history
2026-01-06 11:03
Mathlib/RingTheory/Polynomial/UniversalFactorizationRing.lean
feat(RingTheory): construct etale neighborhood that isolates point in fiber (#32823)
Added
Algebra.exists_etale_bijective_residueFieldMap_and_map_eq_mul_and_isCoprime.{u}
View on Github →