Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-25 06:39 fd036259

View on Github →

chore(ring_theory/ideal): Move local rings into separate file (#8849) Moves the material on local rings and local ring homomorphisms into a separate file and adds a module docstring.

Estimated changes

deleted theorem is_unit_map_iff
deleted theorem is_unit_of_map_unit
deleted theorem local_of_nonunits_ideal
deleted theorem local_of_surjective
deleted theorem local_of_unique_max_ideal
deleted theorem local_ring.nonunits_add
deleted def local_ring.residue
deleted theorem map_nonunit
deleted theorem of_irreducible_map
added theorem is_unit_map_iff
added theorem is_unit_of_map_unit
added theorem local_of_surjective
added theorem map_nonunit
added theorem of_irreducible_map