Theorem IsLocalization.ringEquivOfRingEquiv_symm

Modification history

2025-03-30 21:32
Mathlib/RingTheory/Localization/Defs.lean
refactor(RingTheory): small `erw`-removing refactors to localizations (#23375) …
Modified IsLocalization.ringEquivOfRingEquiv_symmView on Github →
2024-11-13 14:41
Mathlib/RingTheory/Localization/Defs.lean
feat(RingTheory/Localization/*): add `IsLocalization.algEquivOfAlgEquiv` and other results (#18661) …
Added IsLocalization.ringEquivOfRingEquiv_symmView on Github →