Commit 2026-10-02 15:55 ac77769f

View on Github →

chore: address localization algebra TODO (#44422)

Estimated changes

Modified Mathlib/RingTheory/LocalProperties/Basic.lean

deleted theorem Ideal.localized'_eq_map

Modified Mathlib/RingTheory/Localization/Algebra.lean

Modified Mathlib/RingTheory/Localization/Ideal.lean

added theorem Ideal.localized'_eq_map