Theorems · Theorem · linear algebra
Matrix.sum_single_eq_diagonal
∀ {m : Type u_2} {α : Type u_7} [inst : DecidableEq m] [inst_1 : AddCommMonoid α] [inst_2 : Fintype m] (f : m → α),
∑ i, Matrix.single i i (f i) = Matrix.diagonal f- Defined in
- Mathlib.Data.Matrix.Basis
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- AddCommMonoidstatement and proof · cited by 12,281
- Fintypestatement and proof · cited by 7,736
- Finset.sumstatement and proof · cited by 5,195
- Matrixstatement · cited by 4,303
- Finset.univstatement and proof · cited by 3,473
- Matrix.extproof · cited by 540
- Matrix.ofproof · cited by 336
- Matrix.diagonalstatement and proof · cited by 314
- Matrix.singlestatement and proof · cited by 129
- Finset.sum_eq_singleproof · cited by 98
- Matrix.sum_applyproof · cited by 9
Cited by4
Results whose statement or proof uses this declaration.
- Matrix.sum_single_intCastproof · cited by 0
- Matrix.sum_single_natCastproof · cited by 0
- Matrix.sum_single_ofNatproof · cited by 0
- Matrix.sum_single_oneproof · cited by 0