Commit 2025-03-30 21:32 0e2f154d

refactor(RingTheory): small erw-removing refactors to localizations (#23375) This PR contains many small redefinitions in the area of Localization in order to get rid of erws. The main issue is with coercions between types of functions. The main changes are putting some homomorphism coercions in the simp-normal form. This also needs some extra lemmas on those coercions. I think the current mess is a good argument for rethinking the design of FunLike coercions and, in particular, that we currently have Submonoid.map taking any MonoidHomClass.