Theorem Algebra.IsUnramifiedAt.exists_hasStandardEtaleSurjectionOn_of_exists_adjoin_singleton_eq_top

Modification history

2026-02-10 16:30
Mathlib/RingTheory/Unramified/LocalStructure.lean
feat(RingTheory): local structure of unramified algebras (#35023)
Deleted Algebra.IsUnramifiedAt.exists_hasStandardEtaleSurjectionOn_of_exists_adjoin_singleton_eq_topView on Github →
2026-02-06 15:35
Mathlib/RingTheory/Unramified/LocalStructure.lean
feat(RingTheory): local structure of monogenic unramified algebras (#33903)
Added Algebra.IsUnramifiedAt.exists_hasStandardEtaleSurjectionOn_of_exists_adjoin_singleton_eq_topView on Github →