Theorems · Theorem · linear algebra
Matrix.invOf_eq_nonsing_inv
∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α)
[inst_3 : Invertible A], ⅟A = A⁻¹The nonsingular inverse is the same as invOf when A is invertible.
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 102 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- Fintypestatement and proof · cited by 7,736
- Matrixstatement and proof · cited by 4,303
- Matrix.detproof · cited by 665
- Invertiblestatement and proof · cited by 549
- Invertible.invOfstatement and proof · cited by 268
- Matrix.adjugateproof · cited by 64
- Ring.inverse_invertibleproof · cited by 11
- Matrix.inv_defproof · cited by 6
- Matrix.detInvertibleOfInvertibleproof · cited by 3
- Matrix.invOf_eqproof · cited by 1
Cited by11
Results whose statement or proof uses this declaration.
- Matrix.coe_units_invproof · cited by 14
- Matrix.nonsing_inv_mulproof · cited by 12
- Matrix.mul_nonsing_invproof · cited by 11
- Matrix.inv_eq_left_invproof · cited by 9
- Matrix.nonsing_inv_eq_ringInverseproof · cited by 7
- Matrix.det_nonsing_invproof · cited by 4
- Matrix.lieConj_symm_applyproof · cited by 1
- Matrix.inv_submatrix_equivproof · cited by 1
- Matrix.lieConj_applyproof · cited by 0
- Matrix.fromBlocks_eq_of_invertible₂₂proof · cited by 0
- Matrix.GeneralLinearGroup.coe_invproof · cited by 0