Theorems · Theorem · linear algebra

Matrix.kronecker_mulVec_vec_of_commute

∀ {l : Type u_1} {m : Type u_2} {n : Type u_4} {p : Type u_5} {R : Type u_3} [inst : NonUnitalSemiring R]
  [inst_1 : Fintype m] [inst_2 : Fintype n] (A : Matrix l m R) (X : Matrix m n R) (B : Matrix p n R),
  (∀ (x : R) (i : p) (j : n), Commute x (B i j)) →
    (Matrix.kroneckerMap (fun x1 x2 => x1 * x2) B A).mulVec X.vec = (A * X * B.transpose).vec

Technical lemma shared with kronecker_mulVec_vec and vec_mul_eq_mulVec.

Defined in

Mathlib.LinearAlgebra.Matrix.Vec

Cited by

2 results in Mathlib

Foundations

Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NonUnitalSemiringFintypeFintype