Theorems · Theorem · linear algebra
Matrix.det_transpose
∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (M : Matrix n n R),
M.transpose.det = M.detTransposing a matrix preserves the determinant.
- Cited by
- 51 results in Mathlib
- Foundations
- Depth 89 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- DecidableEqFintypeCommRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites20
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- CommRingstatement and proof · cited by 17,173
- Fintypestatement and proof · cited by 7,736
- Finset.sumproof · cited by 5,195
- Matrixstatement and proof · cited by 4,303
- Finset.univproof · cited by 3,473
- Unitsproof · cited by 2,804
- Finset.prodproof · cited by 2,356
- Units.valproof · cited by 1,966
- Equiv.Permproof · cited by 1,375
- Matrix.detstatement and proof · cited by 665
- Matrix.transposestatement and proof · cited by 389
Cited by51
Results whose statement or proof uses this declaration.
- Matrix.det_conjTransposeproof · cited by 7
- Matrix.adjugate_mulproof · cited by 6
- Matrix.det_eq_zero_of_column_eq_zeroproof · cited by 5
- Matrix.adjugate_applyproof · cited by 5
- Matrix.adjugate_transposeproof · cited by 5
- Matrix.det_succ_row_zeroproof · cited by 5
- Algebra.discr_eq_det_embeddingsMatrixReindex_pow_twoproof · cited by 4
- NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasisproof · cited by 4
- Matrix.isTotallyUnimodular_iffproof · cited by 3
- Matrix.transpose_nonsing_invproof · cited by 3
- Matrix.det_fromBlocks_zero₁₂proof · cited by 3
- Matrix.Nondegenerate.of_det_mem_nonZeroDivisorsproof · cited by 3