Commit 2024-10-18 07:51 672f75b1

View on Github →

refactor: rename IsLocalRingHom to IsLocalHom (#17403) Replace the IsLocalRingHom with IsLocalHom. Add instances for IsLocalHom in CommRingCat to resolve the problem caused by #6045. For a more detailed explanation of the problem, see https://github.com/leanprover-community/mathlib4/pull/17403#issuecomment-2418322525. Further golf some proof related to IsLocalHom instance search.

Estimated changes

added theorem isLocalHom_of_isIso
added theorem isLocalHom_of_iso
deleted theorem isLocalRingHom_of_iso
added theorem isLocalHom_equiv
modified theorem IsUnit.of_map
added theorem isLocalHom_toMonoidHom
modified theorem isUnit_map_iff
added theorem isLocalHom_id
added theorem isLocalHom_of_comp
added theorem isLocalHom_toRingHom
deleted theorem isLocalRingHom_of_comp
modified theorem map_nonunit