Theorem LocalRing.residue_surjective

Modification history

2024-11-12 11:09

Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean

chore: rename `LocalRing` to `IsLocalRing` (#18774)

Deleted LocalRing.residue_surjective View on Github →

2024-11-06 12:25

Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean

feat(AlgebraicGeometry): typeclasses for `S`-schemes (#18321)

Added LocalRing.residue_surjective View on Github →