English
The determinant of a Kronecker bilinear map equals the product of determinants of A and B after suitable reshaping, raised to powers given by the sizes of the opposite factors.
Русский
Определитель билинейного отображения Кронекера равен произведению определителей соответствующих преобразований A и B, возведённых в степени, соответствующие размерности противолежащих факторов.
LaTeX
$$$\det(\mathrm{kroneckerMapBilinear} f A B) = \det(A\mapsto f\;\cdot\;1)^{|B|} \cdot \det(B\mapsto f\;1\cdot)^{|A|}$$$
Lean4
/-- `trace` distributes over `Matrix.kroneckerMapBilinear`.
This is primarily used with `R = ℕ` to prove `Matrix.trace_kronecker`. -/
theorem trace_kroneckerMapBilinear [Semiring S] [Semiring R] [Fintype m] [Fintype n] [AddCommMonoid α] [AddCommMonoid β]
[AddCommMonoid γ] [Module R α] [Module R γ] [Module S β] [Module S γ] [SMulCommClass S R γ] (f : α →ₗ[R] β →ₗ[S] γ)
(A : Matrix m m α) (B : Matrix n n β) : trace (kroneckerMapBilinear f A B) = f (trace A) (trace B) := by
simp_rw [Matrix.trace, Matrix.diag, kroneckerMapBilinear_apply_apply, LinearMap.map_sum₂, map_sum, ←
Finset.univ_product_univ, Finset.sum_product, kroneckerMap_apply]
