Theorem RingHom.SurjectiveOnStalks.residueFieldMap_bijective

Modification history

2026-01-22 12:40
Mathlib/RingTheory/LocalRing/ResidueField/Ideal.lean
feat(RingTheory): predicate for `QuasiFiniteAt` (#33718)
Added RingHom.SurjectiveOnStalks.residueFieldMap_bijectiveView on Github →