Theorems · Theorem · linear algebra
Matrix.conjTranspose_nonsing_inv
∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α)
[inst_3 : StarRing α], A⁻¹.conjTranspose = A.conjTranspose⁻¹- Cited by
- 5 results in Mathlib
- Foundations
- Depth 99 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
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
- StarRingstatement and proof · cited by 1,686
- Star.starproof · cited by 1,082
- Matrix.detproof · cited by 665
- Matrix.conjTransposestatement and proof · cited by 202
- Ring.inverseproof · cited by 160
- Matrix.adjugateproof · cited by 64
- Matrix.det_conjTransposeproof · cited by 7
- Matrix.inv_defproof · cited by 6
- Matrix.conjTranspose_smulproof · cited by 5
Cited by5
Results whose statement or proof uses this declaration.
- Matrix.IsHermitian.invproof · cited by 2
- Matrix.conjTranspose_zpowproof · cited by 1
- Matrix.schur_complement_eq₁₁proof · cited by 1
- LDL.lower_conj_diagproof · cited by 0
- Matrix.schur_complement_eq₂₂proof · cited by 0