Theorems · Theorem · group theory
Ring.inverse_invertible
∀ {α : Type u} [inst : MonoidWithZero α] (x : α) [inst_1 : Invertible x], Ring.inverse x = ⅟xA variant of Ring.inverse_unit.
- Defined in
- Mathlib.Algebra.GroupWithZero.Invertible
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 15 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- MonoidWithZeroInvertible
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Invertiblestatement and proof · cited by 549
- MonoidWithZerostatement and proof · cited by 456
- Invertible.invOfstatement · cited by 268
- Ring.inversestatement · cited by 160
- Ring.inverse_unitproof · cited by 24
- unitOfInvertibleproof · cited by 7
Cited by11
Results whose statement or proof uses this declaration.
- Matrix.invOf_eq_nonsing_invproof · cited by 11
- Matrix.nonsing_inv_eq_ringInverseproof · cited by 7
- hasFDerivAt_ringInverseproof · cited by 5
- Matrix.det_nonsing_invproof · cited by 4
- CFC.inverse_eq_rpow_neg_oneproof · cited by 4
- Ring.inverse_expproof · cited by 1
- Matrix.GeneralLinearGroup.det_surjectiveproof · cited by 1
- Ring.inverse_sub_inverseproof · cited by 1
- ContinuousLinearMap.ringInverse_equivproof · cited by 1
- Ring.inverse_add_inverseproof · cited by 1
- Matrix.inv_diagonalproof · cited by 0