Commit 2023-08-11 11:56 68e7a9e8

View on Github →

feat(Algebra/Algebra/Opposite): tools for working with opposite algebras (#6364) This moves the Algebra instance on MulOpposite to a new file, and adds the AlgHom and AlgEquiv versions of various existing RingHom and RingEquiv definitions:

  • AlgHom.fromOpposite
  • AlgHom.toOpposite
  • AlgHom.op
  • AlgHom.unop
  • AlgEquiv.op
  • AlgHom.unop
  • AlgEquiv.toOpposite As MulOpposite.instAlgebra is no longer in Mathlib.Algebra.Algebra.Basic, some new downstream imports are needed.

Estimated changes

added def AlgEquiv.op
added theorem AlgEquiv.toAlgHom_op
added theorem AlgEquiv.toAlgHom_unop
added theorem AlgHom.toRingHom_op
added theorem AlgHom.toRingHom_unop