Theorems · Theorem · linear algebra
Matrix.det_updateRow_sum_aux
∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (M : Matrix n n R)
{j : n} (s : Finset n), j ∉ s → ∀ (c : n → R) (a : R), (M.updateRow j (a • M j + ∑ k ∈ s, c k • M k)).det = a • M.det- Cited by
- 1 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.
Cites21
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
- Finsetstatement and proof · cited by 13,712
- Fintypestatement and proof · cited by 7,736
- Finset.sumstatement and proof · cited by 5,195
- Matrixstatement and proof · cited by 4,303
- add_zeroproof · cited by 2,707
- MulZeroClass.mul_zeroproof · cited by 2,091
- add_commproof · cited by 1,535
- add_assocproof · cited by 746
- Matrix.detstatement and proof · cited by 665
- smul_eq_mulproof · cited by 357
- Finset.sum_insertproof · cited by 196
Cited by1
Results whose statement or proof uses this declaration.
- Matrix.det_updateRow_sumproof · cited by 3