Theorem Algebra.FormallyUnramified.isRadical_map_isMaximal

Modification history

2026-03-26 08:33
Mathlib/RingTheory/Unramified/Field.lean
feat(RingTheory/Unramified/Dedekind): a domain finite and unramified over a Dedekind domain is a Dedekind domain (#36838) …
Added Algebra.FormallyUnramified.isRadical_map_isMaximalView on Github →