Theorem isLocalHom_of_le_jacobson

Modification history

2026-11-02 00:37
Mathlib/RingTheory/Henselian.lean
feat(RingTheory/Jacobson/Ideal): surjective `RingHom` and `IsLocalHom` (#41066) …
Modified isLocalHom_of_le_jacobsonView on Github →
2026-10-28 11:47
Mathlib/RingTheory/Henselian.lean
chore(RingTheory/Jacobson): use `Ring.jacobson` throughout the library (#44788) …
Added isLocalHom_of_le_jacobsonView on Github →