Theorem IsLocalHom.of_surjective

Modification history

2024-11-14 17:15
Mathlib/RingTheory/LocalRing/RingHom/Basic.lean
feat(RingTheory): valuation subrings are maximal local subrings (#19012) …
Added IsLocalHom.of_surjectiveView on Github →