Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-06-29 12:31 e3103498

View on Github →

refactor(ring_theory/ideals): refactor local rings, add local ring homs (#1102)

  • WIP
  • refactor(ring_theory/ideals): refactor local rings, add local ring homs
  • residue_field.map is a field hom
  • make is_local_ring_hom extends is_ring_hom
  • refactor local_ring
  • tiny changes
  • Bump instance search depth

Estimated changes

modified theorem coe_subset_nonunits
modified theorem ideal.is_coprime_def
modified theorem ideal.is_coprime_self
modified theorem ideal.mem_span_pair
modified def is_local_ring
added theorem is_unit_of_map_unit
deleted theorem local_of_nonunits_ideal
added theorem map_nonunit
deleted theorem mem_nonunits_ideal
modified theorem mem_nonunits_iff
modified theorem mul_mem_nonunits_left
modified theorem mul_mem_nonunits_right
modified def nonunits
deleted def nonunits_ideal
modified theorem one_not_mem_nonunits
modified theorem zero_mem_nonunits