Theorem RingHom.isLocalHom_iff_ker_le_jacobson

Modification history

2026-11-02 00:37
Mathlib/RingTheory/Jacobson/Ideal.lean
feat(RingTheory/Jacobson/Ideal): surjective `RingHom` and `IsLocalHom` (#41066) …
Added RingHom.isLocalHom_iff_ker_le_jacobsonView on Github →