Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-27 16:46 2ecf4800

View on Github →

feat(algebra/group/units): generalize units.coe_lift (#11057)

  • Generalize units.coe_lift from group_with_zero to monoid; use condition is_unit instead of ≠ 0.
  • Add some missing @[to_additive] attrs.

Estimated changes

modified theorem is_unit_of_subsingleton