one_kroneckerTMul_one — Mathlib

English

The determinant of a Kronecker product satisfies det(A ⊗ B) = det(A)^{card(B)} ⊗ det(B)^{card(A)} in the appropriate algebraic setting.

Русский

Определитель кронекерового произведения удовлетворяет det(A ⊗ B) = det(A)^{|B|} ⊗ det(B)^{|A|} в соответствующей алгебраической настройке.

LaTeX

$$det (A ⊗ₖₜ[R] B) = (det A ^ card n) ⊗ₜ[R] (det B ^ card m)$$

Lean4

@[simp]
theorem one_kroneckerTMul_one [AddCommMonoidWithOne α] [AddCommMonoidWithOne β] [Module R α] [Module R β]
    [DecidableEq m] [DecidableEq n] : (1 : Matrix m m α) ⊗ₖₜ[R] (1 : Matrix n n β) = 1 :=
  kroneckerMap_one_one _ (zero_tmul _) (tmul_zero _) rfl

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