Theorem RingHom.ker_le_jacobson_of_isLocalHom

Modification history

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