Theorems · Theorem · linear algebra

Matrix.kroneckerMap_add_left

∀ {α : Type u_3} {β : Type u_5} {γ : Type u_7} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12}
  [inst : Add α] [inst_1 : Add γ] (f : α → β → γ),
  (∀ (a₁ a₂ : α) (b : β), f (a₁ + a₂) b = f a₁ b + f a₂ b) →
    ∀ (A₁ A₂ : Matrix l m α) (B : Matrix n p β),
      Matrix.kroneckerMap f (A₁ + A₂) B = Matrix.kroneckerMap f A₁ B + Matrix.kroneckerMap f A₂ B

Defined in

Mathlib.LinearAlgebra.Matrix.Kronecker

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddAdd