English
Trace distributes over Kronecker bilinear map: the trace of kroneckerMapBilinear f A B equals f applied to the traces of A and B.
Русский
След распределяется через билинейное отображение Кронекера: trace(kroneckerMapBilinear f A B) = f(trace A, trace B).
LaTeX
$$$\operatorname{trace}(\mathrm{kroneckerMapBilinear} f A B) = f(\operatorname{trace} A, \operatorname{trace} B)$$$
Lean4
/-- `Matrix.kroneckerMapBilinear` commutes with `*` if `f` does.
This is primarily used with `R = ℕ` to prove `Matrix.mul_kronecker_mul`. -/
theorem kroneckerMapBilinear_mul_mul [Semiring S] [Semiring R] [Fintype m] [Fintype m'] [NonUnitalNonAssocSemiring α]
[NonUnitalNonAssocSemiring β] [NonUnitalNonAssocSemiring γ] [Module R α] [Module R γ] [Module S β] [Module S γ]
[SMulCommClass S R γ] (f : α →ₗ[R] β →ₗ[S] γ) (h_comm : ∀ a b a' b', f (a * b) (a' * b') = f a a' * f b b')
(A : Matrix l m α) (B : Matrix m n α) (A' : Matrix l' m' β) (B' : Matrix m' n' β) :
kroneckerMapBilinear f (A * B) (A' * B') = kroneckerMapBilinear f A A' * kroneckerMapBilinear f B B' :=
by
ext ⟨i, i'⟩ ⟨j, j'⟩
simp only [kroneckerMapBilinear_apply_apply, mul_apply, ← Finset.univ_product_univ, Finset.sum_product,
kroneckerMap_apply]
simp_rw [map_sum f, LinearMap.sum_apply, map_sum, h_comm]
