Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-06 19:21 4f10d1eb

View on Github →

refactor(group_theory/monoid_localization): use characteristic predicate (#2004)

  • should I be changing and committing toml idk
  • initial monoid loc lemmas
  • responding to PR comments
  • removing bad @[simp]
  • inhabited instances
  • remove #lint
  • additive inhabited instance
  • using is_unit & is_add_unit
  • doc string
  • remove simp
  • submonoid.monoid_loc... -> submonoid.localization
  • submonoid.monoid_loc... -> submonoid.localization
  • generalize inhabited instance
  • remove inhabited instance

Estimated changes

added theorem inv_unique
modified theorem is_unit.coe_lift_right
modified theorem is_unit.map
modified theorem is_unit_iff_exists_inv'
modified theorem is_unit_iff_exists_inv
modified theorem is_unit_of_mul_one
modified theorem is_unit_one
modified theorem is_unit_unit
modified theorem units.is_unit_mul_units
added structure add_units
added theorem nat.add_units_eq_one
modified theorem units.coe_inv
modified theorem units.coe_mk_of_mul_eq_one
modified theorem units.coe_mul
modified theorem units.coe_one
modified theorem units.eq_inv_mul_iff_mul_eq
modified theorem units.eq_mul_inv_iff_mul_eq
modified theorem units.ext
modified theorem units.ext_iff
modified theorem units.inv_mul
modified theorem units.inv_mul_cancel_left
modified theorem units.inv_mul_cancel_right
modified theorem units.inv_mul_eq_iff_eq_mul
modified theorem units.mul_inv
modified theorem units.mul_inv_cancel_left
modified theorem units.mul_inv_cancel_right
modified theorem units.mul_inv_eq_iff_eq_mul
modified theorem units.mul_left_inj
modified theorem units.mul_right_inj
modified theorem units.val_coe
modified theorem units.coe_hom_apply
modified theorem units.coe_lift_right
modified theorem units.coe_map
modified theorem units.map_comp
modified theorem units.map_id
deleted theorem add_submonoid.r'.add
deleted def add_submonoid.r'
deleted theorem monoid_localization.ind
deleted theorem monoid_localization.mk_eq
deleted def monoid_localization
deleted def submonoid.r'
deleted def submonoid.r
deleted theorem submonoid.r_eq_r'