Theorems · Theorem · linear algebra
Matrix.mulVec_eq_sum
∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype n] (v : n → α)
(M : Matrix m n α), M.mulVec v = ∑ i, MulOpposite.op (v i) • M.transpose i- Defined in
- Mathlib.Data.Matrix.Mul
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 18 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Fintypestatement and proof · cited by 7,736
- Finset.sumstatement · cited by 5,195
- Matrixstatement and proof · cited by 4,303
- Finset.univstatement and proof · cited by 3,473
- MulOppositestatement · cited by 1,135
- NonUnitalNonAssocSemiringstatement and proof · cited by 1,081
- MulOpposite.opstatement · cited by 520
- Matrix.transposestatement · cited by 389
- Matrix.mulVecstatement · cited by 267
- Finset.sum_fnproof · cited by 21
Cited by12
Results whose statement or proof uses this declaration.
- dotProduct_toMatrix₂_mulVecproof · cited by 2
- OnePoint.smul_some_eq_iteproof · cited by 2
- apply_eq_dotProduct_toMatrix₂_mulVecproof · cited by 2
- Matrix.maxGenEigenspace_toLin_diagonal_eq_eigenspaceproof · cited by 1
- Matrix.permMatrix_mulVecproof · cited by 1
- OnePoint.smul_infty_defproof · cited by 1
- Matrix.fin_two_smul_prodproof · cited by 1
- Matrix.lt_two_mul_of_mul_diagonal_posDef_of_for_le_of_hasEigenproof · cited by 1
- Matrix.inner_toEuclideanCLMproof · cited by 1
- Matrix.isNilpotent_iff_forall_rowproof · cited by 1
- Matrix.mulVec_fin_twoproof · cited by 1
- RootPairing.GeckConstruction.coe_genWeightSpace_zero_eq_span_range_uproof · cited by 0