Theorems · Theorem · linear algebra
single_dotProduct
∀ {m : Type u_2} {α : Type v} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : NonUnitalNonAssocSemiring α]
(v : m → α) (x : α) (i : m), Pi.single i x ⬝ᵥ v = x * v i- Defined in
- Mathlib.Data.Matrix.Mul
- Cited by
- 10 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.
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.sumproof · cited by 5,195
- Finset.univproof · cited by 3,473
- MulZeroClass.zero_mulproof · cited by 1,625
- NonUnitalNonAssocSemiringstatement and proof · cited by 1,081
- Pi.singlestatement and proof · cited by 518
- dotProductstatement and proof · cited by 194
- Pi.single_eq_sameproof · cited by 144
- Pi.single_eq_of_neproof · cited by 116
- Finset.sum_eq_singleproof · cited by 98
Cited by10
Results whose statement or proof uses this declaration.
- Matrix.single_vecMulproof · cited by 4
- ProbabilityTheory.covariance_eval_multivariateGaussianproof · cited by 3
- Matrix.separatingRight_iff_forall_mulVec_eq_zeroproof · cited by 2
- range_vecMulLinearproof · cited by 2
- exists_ne_zero_dotProduct_eq_zeroproof · cited by 2
- ProbabilityTheory.measurePreserving_restrict₂_multivariateGaussianproof · cited by 1
- FirstOrder.Language.presburger.term_realize_eq_add_dotProductproof · cited by 1
- Pi.counit_eq_adjointproof · cited by 0
- single_one_dotProductproof · cited by 0
- Pi.comul_eq_adjointproof · cited by 0