Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-31 10:19 31c8aa59

View on Github →

chore(algebra/group_with_zero/basic): zero, one, and pow lemmas for ring.inverse (#10049) This adds:

  • ring.inverse_zero
  • ring.inverse_one
  • ring.inverse_pow (to match inv_pow, inv_pow₀)
  • commute.ring_inverse_ring_inverse (to match commute.inv_inv)

Estimated changes

added theorem ring.inverse_one
added theorem ring.inverse_zero
added theorem ring.mul_inverse_rev'
modified theorem ring.mul_inverse_rev
added theorem ring.inverse_pow