det_kronecker — Mathlib

English

For finite index types m,n and commutative ring R, det(A ⊗ B) = det(A)^{card n} · det(B)^{card m}.

Русский

Пусть индексы конечны m,n и R — коммутативное кольцо. Тогда det(A ⊗ B) = det(A)^{card(n)} · det(B)^{card(m)}.

LaTeX

$$$$ \\det(A \\otimes B) = \\det(A)^{\\#n} \\cdot \\det(B)^{\\#m} $$$$

Lean4

theorem det_kronecker [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing R] (A : Matrix m m R)
    (B : Matrix n n R) : det (A ⊗ₖ B) = det A ^ Fintype.card n * det B ^ Fintype.card m :=
  by
  refine (det_kroneckerMapBilinear (Algebra.lmul ℕ R).toLinearMap mul_mul_mul_comm _ _).trans ?_
  congr 3
  · ext i j
    exact mul_one _
  · ext i j
    exact one_mul _

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