Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-20 09:21 68b9c164

View on Github →

feat(algebra/group): add units.lift_right and is_unit.lift_right (#2020)

  • Rename type variables, add a docstring
  • feat(algebra/group): add units.lift_right and is_unit.lift_right These defs/lemmas may be useful for monoid_localization.

Estimated changes

added theorem is_unit.coe_lift_right
modified def units.coe_hom
modified theorem units.coe_hom_apply
added theorem units.coe_lift_right
modified theorem units.coe_map'
modified theorem units.coe_map
added def units.lift_right
modified def units.map'
modified def units.map
modified theorem units.map_comp
modified theorem units.map_id