Commit 2023-07-24 10:54 30c87ba5

View on Github →

feat(Algebra.Ring.Equiv) : provide RingHom inverse (#5997) Define:

  • OneHom.inverse (and its additive version)
  • NonUnitalRingHom.inverse
  • RingHom.inverse

Estimated changes

modified def MulHom.inverse
added def OneHom.inverse
added def RingHom.inverse