Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-27 17:10 b86c528d

View on Github →

feat(ring_theory/ideal/local_ring): API for local rings. (#17185)

Estimated changes

Modified src/algebraic_geometry/prime_spectrum/basic.lean

added theorem local_ring.closed_point_mem_iff

added theorem local_ring.specializes_closed_point

added theorem prime_spectrum.comap_residue

Modified src/ring_theory/discrete_valuation_ring.lean

Modified src/ring_theory/ideal/basic.lean

added theorem ring.is_field_iff_is_simple_order_ideal

deleted theorem ring.not_is_field_of_subsingleton

Modified src/ring_theory/ideal/local_ring.lean

added theorem local_ring.is_field_iff_maximal_ideal_eq

added theorem local_ring.maximal_ideal_eq_bot

added def local_ring.residue_field.lift

added theorem local_ring.residue_field.lift_comp_residue

added theorem local_ring.residue_field.lift_residue_apply

Modified src/ring_theory/ideal/operations.lean

Modified src/ring_theory/localization/at_prime.lean

added theorem is_localization.at_prime.comap_maximal_ideal