Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-15 15:03 2194eef2

View on Github →

chore(ring_theory/ideal/local_ring): generalize to semirings (#13341)

Estimated changes

Modified src/logic/equiv/transfer_instance.lean

Modified src/number_theory/padics/padic_integers.lean

Modified src/ring_theory/discrete_valuation_ring.lean

Modified src/ring_theory/graded_algebra/homogeneous_localization.lean

Modified src/ring_theory/ideal/local_ring.lean

modified theorem is_local_ring_hom_of_comp

modified theorem is_unit_map_iff

modified 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_of_unique_nonzero_prime

modified theorem local_ring.is_unit_of_mem_nonunits_one_sub_self

modified theorem local_ring.is_unit_or_is_unit_one_sub_self

modified theorem local_ring.ker_eq_maximal_ideal

modified theorem local_ring.maximal_ideal_unique

modified theorem local_ring.mem_maximal_ideal

deleted theorem local_ring.nonunits_add

added theorem local_ring.of_is_unit_or_is_unit_one_sub_self

added theorem local_ring.of_surjective

added theorem local_ring.of_unique_max_ideal

added theorem local_ring.of_unique_nonzero_prime

added theorem map_mem_nonunits_iff

modified theorem map_nonunit

modified theorem of_irreducible_map

modified theorem ring_hom.domain_local_ring

Modified src/ring_theory/localization/at_prime.lean

Modified src/ring_theory/power_series/basic.lean

Modified src/ring_theory/valuation/valuation_ring.lean