LeanPool.RlTheoryInLean.Data.Matrix.Mul

theorem Matrix.mul_diagonal_mulVec {m : Type u_1} {n : Type u_2} [DecidableEq n] [Fintype n] (d x : n → ℝ) (A : Matrix m n ℝ) : (A * diagonal d).mulVec x = ∑ i : n, d i • x i • A.col i

theorem Matrix.mulVec_apply {m : Type u_1} {n : Type u_2} [Fintype n] (A : Matrix m n ℝ) (x : n → ℝ) (j : m) : A.mulVec x j = ∑ i : n, A j i * x i

theorem Matrix.dotProduct_transpose_mulVec_real {m : Type u_1} [Fintype m] {A : Matrix m m ℝ} (x y : m → ℝ) : x ⬝ᵥ A.transpose.mulVec y = y ⬝ᵥ A.mulVec x

theorem Matrix.vecMul_diagonal_dotProduct {m : Type u_1} [Fintype m] [DecidableEq m] (d x y : m → ℝ) : vecMul x (diagonal d) ⬝ᵥ y = ∑ i : m, d i * x i * y i