Theorems · Theorem · linear algebra

Matrix.det_kroneckerTMul

∀ (R : Type u_1) {α : Type u_3} {β : Type u_5} {m : Type u_10} {n : Type u_11} [inst : CommRing R] [inst_1 : CommRing α]
  [inst_2 : CommRing β] [inst_3 : Algebra R α] [inst_4 : Algebra R β] [inst_5 : Fintype m] [inst_6 : Fintype n]
  [inst_7 : DecidableEq m] [inst_8 : DecidableEq n] (A : Matrix m m α) (B : Matrix n n β),
  (Matrix.kroneckerMap (TensorProduct.tmul R) A B).det = (A.det ^ Fintype.card n) ⊗ₜ[R] (B.det ^ Fintype.card m)

Defined in

Mathlib.LinearAlgebra.Matrix.Kronecker

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingCommRingCommRingAlgebraAlgebraFintypeFintypeDecidableEqDecidableEq