Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-25 16:36 db7a53af

View on Github →

refactor(ring_theory/ideals): make local_ring a prop class (#3171)

Estimated changes

Modified src/ring_theory/ideals.lean

deleted def is_local_ring

deleted def local_of_is_local_ring

added theorem local_of_nonunits_ideal

deleted def local_of_nonunits_ideal

added theorem local_of_unique_max_ideal

deleted def local_of_unique_max_ideal

deleted def local_of_unit_or_unit_one_sub

added def local_ring.maximal_ideal

added theorem local_ring.mem_maximal_ideal

deleted theorem local_ring.mem_nonunits_ideal

deleted def local_ring.nonunits_ideal

modified def local_ring.residue_field

modified theorem map_nonunit

Modified src/ring_theory/power_series.lean

deleted theorem mv_power_series.is_local_ring

deleted theorem power_series.is_local_ring