Theorem IsLocalRing.map_maximalIdeal_of_surjective

Modification history

2026-03-20 18:13
Mathlib/RingTheory/LocalRing/RingHom/Basic.lean
feat(RingTheory): some lemma about span rank (#35337) …
Added IsLocalRing.map_maximalIdeal_of_surjectiveView on Github →