Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-04 08:58 1691c6c2

View on Github →

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

Estimated changes

Modified src/algebra/opposites.lean

added def add_equiv.op

added def add_equiv.unop

added def mul_equiv.op

added def mul_equiv.unop

Modified src/data/equiv/ring.lean