Commit 2019-03-22 00:28 989efaba
View on Github →feat(data/equiv/algebra): add add_equiv and mul_equiv (#789)
- feat(data/equiv/algebra): add monoid_equiv and group_equiv
- refactor; now using mul_equiv; adding add_equiv
- tidy
- namechange broke my code; now fixed
- next effort
- switching is_mul_hom back to explicit args
- removing more implicits
- typo
- switching back to implicits (to fix mathlib breakage)
- Making is_mul_hom and is_add_hom classes
- adding more to_additive