Theorems · Theorem · linear algebra

Matrix.add_kronecker

∀ {α : Type u_3} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} [inst : Distrib α]
  (A₁ A₂ : Matrix l m α) (B : Matrix n p α),
  Matrix.kroneckerMap (fun x1 x2 => x1 * x2) (A₁ + A₂) B =
    Matrix.kroneckerMap (fun x1 x2 => x1 * x2) A₁ B + Matrix.kroneckerMap (fun x1 x2 => x1 * x2) A₂ B

Defined in

Mathlib.LinearAlgebra.Matrix.Kronecker

Cited by

0 results in Mathlib

Foundations

Depth 16 from the axioms · uses propext, Quot.sound

Assumes

Distrib