trace_kroneckerTMul — Mathlib

English

The trace of the Kronecker product equals the tensor product of traces: tr(A ⊗_R B) = tr(A) ⊗_R tr(B).

Русский

След кронекерового произведения равен тензорному произведению следов: tr(A ⊗ B) = tr(A) ⊗ tr(B).

LaTeX

$$trace (A ⊗ₖₜ[R] B) = trace A ⊗ₜ[R] trace B$$

Lean4

theorem trace_kroneckerTMul [Fintype m] [Fintype n] (A : Matrix m m α) (B : Matrix n n β) :
    trace (A ⊗ₖₜ[R] B) = trace A ⊗ₜ[R] trace B :=
  trace_kroneckerMapBilinear (TensorProduct.mk R α β) _ _

Похожие утверждения