Theorems · Theorem · linear algebra

Matrix.trace_kroneckerTMul

∀ (R : Type u_1) {α : Type u_3} {β : Type u_5} {m : Type u_10} {n : Type u_11} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid α] [inst_2 : AddCommMonoid β] [inst_3 : Module R α] [inst_4 : Module R β] [inst_5 : Fintype m]
  [inst_6 : Fintype n] (A : Matrix m m α) (B : Matrix n n β),
  (Matrix.kroneckerMap (TensorProduct.tmul R) A B).trace = A.trace ⊗ₜ[R] B.trace

Defined in

Mathlib.LinearAlgebra.Matrix.Kronecker

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidAddCommMonoidModuleModuleFintypeFintype