mathlib3
2ecf4800
- feat(algebra/group/units): generalize `units.coe_lift` (#11057)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
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.
Author
urkud
Parents
de6f57d2
Loading