English
Mixing scalar actions on the left distributes over Kronecker: (r · A) ⊗ B = r · (A ⊗ B).
Русский
Действие скаляра слева распадается на разложение по Kronecker: (r · A) ⊗ B = r · (A ⊗ B).
LaTeX
$$ (r • A) ⊗ₖₜ[R] B = r • A ⊗ₖₜ[R] B$$
Lean4
theorem det_kroneckerTMul [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (A : Matrix m m α)
(B : Matrix n n β) : det (A ⊗ₖₜ[R] B) = (det A ^ Fintype.card n) ⊗ₜ[R] (det B ^ Fintype.card m) :=
by
refine (det_kroneckerMapBilinear (TensorProduct.mk R α β) tmul_mul_tmul _ _).trans ?_
simp -eta only [mk_apply, ← includeLeft_apply (S := R), ← includeRight_apply]
simp only [← AlgHom.mapMatrix_apply, ← AlgHom.map_det]
simp only [includeLeft_apply, includeRight_apply, tmul_pow, tmul_mul_tmul, one_pow, _root_.mul_one, _root_.one_mul]
