Theorems · Theorem · linear algebra

Matrix.single_kroneckerTMul_single

∀ (R : Type u_1) {α : Type u_3} {β : Type u_5} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12}
  [inst : CommSemiring R] [inst_1 : AddCommMonoid α] [inst_2 : AddCommMonoid β] [inst_3 : Module R α]
  [inst_4 : Module R β] [inst_5 : DecidableEq l] [inst_6 : DecidableEq m] [inst_7 : DecidableEq n]
  [inst_8 : DecidableEq p] (i₁ : l) (j₁ : m) (i₂ : n) (j₂ : p) (a : α) (b : β),
  Matrix.kroneckerMap (TensorProduct.tmul R) (Matrix.single i₁ j₁ a) (Matrix.single i₂ j₂ b) =
    Matrix.single (i₁, i₂) (j₁, j₂) (a ⊗ₜ[R] b)

Defined in

Mathlib.LinearAlgebra.Matrix.Kronecker

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidAddCommMonoidModuleModuleDecidableEqDecidableEqDecidableEqDecidableEq