English
The bilinear Kronecker map commutes with simultaneous index automorphisms: kroneckerMap f (reindex el em M) (reindex en ep N) equals the reindexed kroneckerMap f M N by the appropriate product equivalences.
Русский
Кронекерово билинейное отображение commute с одновременными преобразованиями индексов: kroneckerMap f (reindex el em M) (reindex en ep N) = reindex (el.prodCongr en) (em.prodCongr ep) (kroneckerMap f M N).
LaTeX
$$$\operatorname{kroneckerMap} f (\mathrm{reindex}\ el\ em\ M) (\mathrm{reindex}\ en\ ep\ N) = \mathrm{reindex} (el.prodCongr en) (em.prodCongr ep) (\operatorname{kroneckerMap} f M N)$$$
Lean4
theorem kroneckerMap_reindex (f : α → β → γ) (el : l ≃ l') (em : m ≃ m') (en : n ≃ n') (ep : p ≃ p') (M : Matrix l m α)
(N : Matrix n p β) :
kroneckerMap f (reindex el em M) (reindex en ep N) =
reindex (el.prodCongr en) (em.prodCongr ep) (kroneckerMap f M N) :=
by
ext ⟨i, i'⟩ ⟨j, j'⟩
rfl
