Def LocalRing.closedPoint

Modification history

2024-11-12 11:09

Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

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

Deleted LocalRing.closedPoint View on Github →

2023-05-24 09:36

Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

feat: port AlgebraicGeometry.PrimeSpectrum.Basic (#4276)

Added LocalRing.closedPoint View on Github →