Commit 2020-05-19 07:10 52aa1281
View on Github →feat(data/equiv): add add_equiv.to_multiplicative (#2732)
We already have add_monoid_hom.to_multiplicative. This adds add_equiv.to_multiplicative.
It is placed in data/equiv/mul_add.lean because data/equiv/mul_add.lean already imports algebra/group/type_tags.lean.