A few small Matrix lemmas

Stream: Is there code for X?

[Snir Broshi]

Do any of these lemmas exist in some form somewhere?

import Mathlib
open Matrix
variable {R : Type*} [CommRing R]
variable {n : Type*} [DecidableEq n] [Fintype n]
variable {m : Type*} [DecidableEq m] [Fintype m]
variable (M : Matrix n n R)
variable (v : n → R)
variable (a : R)

@[simp]
lemma algebraMap_eq_scalar : algebraMap R (Matrix n n R) a = scalar n a :=
  rfl

lemma scalar_mulVec_eq_smul : scalar n a *ᵥ v = a • v := by
  simp

lemma scalar_vecMul_eq_smul : v ᵥ* scalar n a = a • v := by
  simp

lemma ne_zero_iff_exists_mulVec_ne_zero : M ≠ 0 ↔ ∃ v, M *ᵥ v ≠ 0 := by
  sorry

lemma ne_zero_iff_exists_vecMul_ne_zero : M ≠ 0 ↔ ∃ v, v ᵥ* M ≠ 0 := by
  sorry

lemma eq_zero_iff_forall_mulVec_eq_zero : M = 0 ↔ ∀ v, M *ᵥ v = 0 := by
  sorry

lemma eq_zero_iff_forall_vecMul_eq_zero : M = 0 ↔ ∀ v, v ᵥ* M = 0 := by
  sorry

@[simp]
lemma Finset.sum_mulVec_distrib {ι : Type*} {s : Finset ι} {f : ι → Matrix m n R} :
    (∑ x ∈ s, f x) *ᵥ v = ∑ x ∈ s, (f x *ᵥ v) := by
  sorry

@[simp]
lemma Finset.sum_vecMul_distrib {ι : Type*} {s : Finset ι} {f : ι → Matrix n m R} :
    v ᵥ* (∑ x ∈ s, f x) = ∑ x ∈ s, (v ᵥ* f x) := by
  sorry

[Eric Wieser]

I think @Monica Omar has a PR with the last two

[Eric Wieser]

algebraMap_eq_scalar is probably a bad simp lemma; really we want to unify algebraMap and scalar to be one and the same

[Eric Wieser]

scalar_vecMul_eq_smul should be stated with MulOpposite.op, so that it holds in non-commutative rings

[Monica Omar]

Since this is in a commutative ring, the last two are already known:

import Mathlib

open Matrix
variable {R : Type*} [CommRing R]
variable {n : Type*} [Fintype n]
variable {m : Type*}
variable (M : Matrix n n R)
variable (v : n → R)

lemma Finset.sum_mulVec_distrib {ι : Type*} {s : Finset ι} {f : ι → Matrix m n R} :
    (∑ x ∈ s, f x) *ᵥ v = ∑ x ∈ s, (f x *ᵥ v) :=
  LinearMap.map_sum₂ (mulVecBilin R R) s f v

lemma Finset.sum_vecMul_distrib {ι : Type*} {s : Finset ι} {f : ι → Matrix n m R} :
    v ᵥ* (∑ x ∈ s, f x) = ∑ x ∈ s, (v ᵥ* f x) :=
  map_sum ((vecMulBilin R R) v) f s