mathlib
d219e6bb - chore(data/equiv/mul_add): DRY (#10150)

Commit
4 years ago
chore(data/equiv/mul_add): DRY (#10150) use `units.mul_left`/`units.mul_right` to define `equiv.mul_leftâ‚€`/`equiv.mul_rightâ‚€`.
Author
Parents
Loading