Commit 2024-10-08 12:10 546cfa08
View on Github →refactor: generalise IsLocalRingHom to monoids (#6045)
This lets IsLocalRingHom take two monoids instead of rings. Furthermore, it moves lemmas to be available a bit earlier where they are relevant to other theories, and tries to adapt those theories to use them a bit better.