mathlib
6e64df5f
- chore(deprecated/group): Do not import `deprecated` from `equiv/mul_add` (#4989)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
5 years ago
chore(deprecated/group): Do not import `deprecated` from `equiv/mul_add` (#4989) This swaps the direction of the import, which makes the deprecated instances for `mul_equiv` be in the same place as the instances for `monoid_hom`.
Author
eric-wieser
Parents
97a7f577
Loading