Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-28 20:55 05449a06

View on Github →

refactor(ring_theory/localization): rename of to mk, and define of (#765)

  • refactor(ring_theory/localization): rename of to mk, and define of
  • Make submonoid implicit variable of 'of'

Estimated changes

deleted theorem localization.coe_mul_of
added def localization.mk
added theorem localization.mk_eq_div
added theorem localization.mk_mul_mk
added theorem localization.mk_self''
added theorem localization.mk_self'
added theorem localization.mk_self
modified def localization.of
modified theorem localization.of_add
deleted theorem localization.of_eq_div
modified theorem localization.of_mul
deleted theorem localization.of_mul_of
modified theorem localization.of_neg
modified theorem localization.of_one
modified theorem localization.of_pow
deleted theorem localization.of_self''
deleted theorem localization.of_self'
deleted theorem localization.of_self
modified theorem localization.of_sub
modified theorem localization.of_zero