Theorems · Theorem · linear algebra
Matrix.vec_sum
∀ {ι : Type u_2} {m : Type u_3} {n : Type u_4} {R : Type u_1} [inst : AddCommMonoid R] (s : Finset ι)
(A : ι → Matrix m n R), (∑ i ∈ s, A i).vec = ∑ i ∈ s, (A i).vec- Defined in
- Mathlib.LinearAlgebra.Matrix.Vec
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 18 from the axioms · uses propext, Quot.sound
- Assumes
- AddCommMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement and proof · cited by 13,712
- AddCommMonoidstatement and proof · cited by 12,281
- Finset.sumstatement and proof · cited by 5,195
- Matrixstatement and proof · cited by 4,303
- Finset.sum_applyproof · cited by 234
- Matrix.vecstatement and proof · cited by 27
- Matrix.sum_applyproof · cited by 9
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.