Theorems · Theorem · linear algebra

Matrix.mul_kronecker_mul

∀ {α : Type u_3} {l : Type u_9} {m : Type u_10} {n : Type u_11} {l' : Type u_15} {m' : Type u_16} {n' : Type u_17}
  [inst : Fintype m] [inst_1 : Fintype m'] [inst_2 : CommSemiring α] (A : Matrix l m α) (B : Matrix m n α)
  (A' : Matrix l' m' α) (B' : Matrix m' n' α),
  Matrix.kroneckerMap (fun x1 x2 => x1 * x2) (A * B) (A' * B') =
    Matrix.kroneckerMap (fun x1 x2 => x1 * x2) A A' * Matrix.kroneckerMap (fun x1 x2 => x1 * x2) B B'

Defined in

Mathlib.LinearAlgebra.Matrix.Kronecker

Cited by

2 results in Mathlib

Foundations

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

Assumes

FintypeFintypeCommSemiring