mathlib3
52aa1281 - feat(data/equiv): add add_equiv.to_multiplicative (#2732)

Commit
6 years ago
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`.
Author
Parents
Loading