Def RingHom.toLocalizationIsMaximalEquiv

Modification history

2024-12-10 08:25
Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean
feat: PrimeSpectrum has DiscreteTopology iff toLocalization is bijective (#19714) …
Deleted RingHom.toLocalizationIsMaximalEquivView on Github →
2024-11-26 22:40
Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean
feat: semiring with discrete PrimeSpectrum (#19496) …
Modified RingHom.toLocalizationIsMaximalEquivView on Github →
2024-11-25 16:30
Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean
feat: ring with discrete PrimeSpectrum (#18891) …
Added RingHom.toLocalizationIsMaximalEquivView on Github →