Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-06 14:21 cc753d7b

View on Github →

feat(ring_theory/localization): adds induced ring hom between fraction rings (#781)

  • feat(ring_theory/localization): adds induced ring hom between fraction rings
  • Break some extremely long lines
  • Put map in the fraction_ring namespace
  • Move global variable into statements
  • Rename rec to lift', make interface for lift, generalise map
  • Improve simp-lemmas, add docstrings
  • Rename circ to comp in lemma names

Estimated changes

modified def localization.at_prime
modified def localization.away
modified theorem localization.coe_add
modified theorem localization.coe_mul
modified theorem localization.coe_neg
modified theorem localization.coe_one
modified theorem localization.coe_pow
modified theorem localization.coe_sub
modified theorem localization.coe_zero
deleted theorem localization.eq_zero_of
added theorem localization.lift'_coe
added theorem localization.lift'_of
added theorem localization.lift_coe
added theorem localization.lift_of
deleted def localization.loc
added def localization.map
added theorem localization.map_coe
modified theorem localization.map_comap
added theorem localization.map_of
modified def localization.mk
added theorem localization.mk_eq
deleted theorem localization.mk_eq_div
deleted theorem localization.of.injective
modified def localization.of
modified theorem localization.of_add
modified theorem localization.of_mul
modified theorem localization.of_neg
modified theorem localization.of_one
modified theorem localization.of_pow
modified theorem localization.of_sub
modified theorem localization.of_zero
added def localization