Theorem Ideal.localized'_eq_map

Modification history

2026-10-02 15:55
Mathlib/RingTheory/LocalProperties/Basic.lean
chore: address localization algebra TODO (#44422)
Modified Ideal.localized'_eq_mapView on Github →
2024-11-26 20:08
Mathlib/RingTheory/LocalProperties/Basic.lean
chore(RingTheory/Localization): golfs and generalizations (#19310) …
Added Ideal.localized'_eq_mapView on Github →