Commit 2026-05-01 19:07 24972cd4
View on Github →refactor(Localization/AtPrime/Basic): add predicate for algebra instance on Localization.AtPrime (#38465)
Currently Localization.AtPrime induces a diamond when the top ring is already an algebra over the localization of the bottom ring (e.g., this happens for Ideal.Fiber). This PR resolves the diamond by turning the instance into a def and adding a predicate typeclass.
Zulip thread: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/instance.20diamond.20with.20.60Ideal.2EFiber.60