Theorems · Theorem · linear algebra
Matrix.mulVec_single
∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} [inst : Fintype n] [inst_1 : DecidableEq n]
[inst_2 : NonUnitalNonAssocSemiring R] (M : Matrix m n R) (j : n) (x : R),
M.mulVec (Pi.single j x) = MulOpposite.op x • M.col j- Defined in
- Mathlib.Data.Matrix.Mul
- Cited by
- 23 results in Mathlib
- Foundations
- Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
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
- Matrixstatement and proof · cited by 4,303
- MulOppositestatement · cited by 1,135
- NonUnitalNonAssocSemiringstatement and proof · cited by 1,081
- MulOpposite.opstatement · cited by 520
- Pi.singlestatement · cited by 518
- Matrix.mulVecstatement · cited by 267
- Matrix.colstatement · cited by 56
- dotProduct_singleproof · cited by 2
Cited by23
Results whose statement or proof uses this declaration.
- Matrix.mulVec_single_oneproof · cited by 5
- ProbabilityTheory.covariance_eval_multivariateGaussianproof · cited by 3
- Matrix.separatingLeft_iff_forall_vecMul_eq_zeroproof · cited by 2
- Matrix.mulVecLin_oneproof · cited by 2
- LieModule.toEnd_matrixproof · cited by 2
- RootPairing.GeckConstruction.isNilpotent_eproof · cited by 2
- Matrix.isNilpotent_iff_forall_rowproof · cited by 1
- Matrix.mulVec_injectiveproof · cited by 1
- ProbabilityTheory.measurePreserving_restrict₂_multivariateGaussianproof · cited by 1
- PiToModule.fromMatrix_apply_single_oneproof · cited by 1
- Matrix.l2_opNorm_diagonalproof · cited by 1
- RootPairing.Base.det_four_sub_cartanMatrix_ne_zeroproof · cited by 0