Theorems · Theorem · linear algebra
Matrix.det_succ_row
∀ {R : Type v} [inst : CommRing R] {n : ℕ} (A : Matrix (Fin n.succ) (Fin n.succ) R) (i : Fin n.succ),
A.det = ∑ j, (-1) ^ (↑i + ↑j) * A i j * (A.submatrix i.succAbove j.succAbove).detLaplacian expansion of the determinant of an n+1 × n+1 matrix along row i.
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites29
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
- Finset.sumstatement and proof · cited by 5,195
- Matrixstatement and proof · cited by 4,303
- Finset.univstatement and proof · cited by 3,473
- one_mulproof · cited by 2,841
- Finset.sum_congrproof · cited by 2,323
- Units.valproof · cited by 1,966
- mul_assocproof · cited by 1,667
- Matrix.detstatement and proof · cited by 665
- Int.cast_oneproof · cited by 371
- pow_addproof · cited by 315
Cited by6
Results whose statement or proof uses this declaration.
- Matrix.adjugate_fin_succ_eq_det_submatrixproof · cited by 2
- Matrix.det_eq_sum_column_mul_submatrix_succAbove_succAbove_detproof · cited by 1
- Matrix.det_eq_sum_mul_adjugate_rowproof · cited by 1
- Matrix.IsTotallyUnimodular.fromRows_unitlikeproof · cited by 1
- Polynomial.resultant_succ_left_degproof · cited by 1
- Matrix.det_succ_columnproof · cited by 0