mathlib3
e174f42c - feat(equiv/transfer_instances): other algebraic structures (#3870)

Commit
5 years ago
feat(equiv/transfer_instances): other algebraic structures (#3870) Some updates to `data.equiv.transfer_instances`. 1. Use `@[to_additive]` 2. Add algebraic equivalences between the original and transferred instances. 3. Transfer modules and algebras. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading