Commit 2026-11-02 00:37 b6dfe53c
View on Github →feat(RingTheory/Jacobson/Ideal): surjective RingHom and IsLocalHom (#41066)
This is a split of #41064 which shows that a surjective RingHom is a local homomorphism if and only if its kernel is contained in the jacobson radical of the ring.