trace_kronecker — Mathlib

English

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

Русский

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

LaTeX

$$$$ \\operatorname{tr}(A \\otimes B) = \\operatorname{tr}(A) \\cdot \\operatorname{tr}(B) $$$$

Lean4

theorem trace_kronecker [Fintype m] [Fintype n] [Semiring α] (A : Matrix m m α) (B : Matrix n n α) :
    trace (A ⊗ₖ B) = trace A * trace B :=
  trace_kroneckerMapBilinear (Algebra.lmul ℕ α).toLinearMap _ _

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