Commit 2026-03-24 16:45 05876211

View on Github →

feat: notation for Ring.inverse (#34396) This PR adds the notation x⁻¹ʳ for Ring.inverse x, scoped to the namespace Ring, and a few extra API lemmas about it. See the Zulip discussion about this.

Estimated changes

modified theorem Ring.inverse_pow
modified theorem Ring.inverse_invertible
modified theorem IsUnit.ringInverse
modified theorem Ring.inverse_eq_inv
added theorem Ring.inverse_inverse
modified theorem Ring.inverse_mul_cancel
modified theorem Ring.inverse_non_unit
modified theorem Ring.inverse_of_isUnit
modified theorem Ring.inverse_one
modified theorem Ring.inverse_unit
modified theorem Ring.inverse_zero
modified theorem Ring.mul_inverse_cancel
modified theorem isUnit_ringInverse
added theorem cfc_ringInverse_id
modified theorem Ring.inverse_exp
modified theorem Matrix.det_nonsing_inv
modified theorem Matrix.inv_def
modified theorem Matrix.inv_diagonal
modified theorem MulChar.inv_apply_eq_inv