Theorems · Theorem · linear algebra

Matrix.kroneckerMap_diagonal_left

∀ {α : Type u_3} {β : Type u_5} {γ : Type u_7} {l : Type u_9} {m : Type u_10} {n : Type u_11} [inst : Zero α]
  [inst_1 : Zero γ] [inst_2 : DecidableEq l] (f : α → β → γ),
  (∀ (b : β), f 0 b = 0) →
    ∀ (a : l → α) (B : Matrix m n β),
      Matrix.kroneckerMap f (Matrix.diagonal a) B =
        (Matrix.reindex (Equiv.prodComm m l) (Equiv.prodComm n l))
          (Matrix.blockDiagonal fun i => B.map fun b => f (a i) b)

Defined in

Mathlib.LinearAlgebra.Matrix.Kronecker

Cited by

3 results in Mathlib

Foundations

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

Assumes

ZeroZeroDecidableEq