Units and Jacobson radical

Stream: Is there code for X?

[Adam Topaz]

I'm playing with @Johan Commelin 's Henselian local rings branch, and trying out some possible generalizations.
Do we have a lemma along the following lines?

lemma local_map_of_le_jacobson {R : Type*} [comm_ring R] {I : ideal R}
  (h : I ≤ ideal.jacobson ⊥) : is_local_ring_hom (ideal.quotient.mk I) :=

[Adam Topaz]

(well, it should be generalized a bit replacing I with the kernel of a ring hom)