Commit 2022-12-15 14:12 69e54061

View on Github →

feat port: algebra.ring.opposite (#977)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Ring/Opposite.lean

added def NonUnitalRingHom.fromOpposite

added def NonUnitalRingHom.op

added def NonUnitalRingHom.toOpposite

added def NonUnitalRingHom.unop

added def RingHom.fromOpposite

added def RingHom.op

added def RingHom.toOpposite

added def RingHom.unop