mathlib
1691c6c2 - feat(algebra/opposites): {add,mul,ring}_equiv.op (#8535)

Commit

4 years ago

feat(algebra/opposites): {add,mul,ring}_equiv.op (#8535) We had the equivalences of homs. Now we have equivalences of isos.

Author

pechersky

Parents