Theorems · Theorem · linear algebra

Matrix.kroneckerMap_diagonal_diagonal

∀ {α : Type u_3} {β : Type u_5} {γ : Type u_7} {m : Type u_10} {n : Type u_11} [inst : Zero α] [inst_1 : Zero β]
  [inst_2 : Zero γ] [inst_3 : DecidableEq m] [inst_4 : DecidableEq n] (f : α → β → γ),
  (∀ (b : β), f 0 b = 0) →
    (∀ (a : α), f a 0 = 0) →
      ∀ (a : m → α) (b : n → β),
        Matrix.kroneckerMap f (Matrix.diagonal a) (Matrix.diagonal b) = Matrix.diagonal fun mn => f (a mn.1) (b mn.2)

Defined in

Mathlib.LinearAlgebra.Matrix.Kronecker

Cited by

3 results in Mathlib

Foundations

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

Assumes

ZeroZeroZeroDecidableEqDecidableEq