English
If el is an index equivalence on l, then kroneckerMap f (reindex el em M) N equals reindex ... (kroneckerMap f M N).
Русский
Пусть el — эквивалент индексов на l; тогда kroneckerMap f (reindex el em M) N эквивалентно reindex ... (kroneckerMap f M N).
LaTeX
$$$\operatorname{kroneckerMap} f (\mathrm{Matrix.reindex}\ el em\ M) N = \mathrm{reindex} (el.prodCongr (\mathrm{Equiv.refl} _)) (em.prodCongr (\mathrm{Equiv.refl} _)) (\operatorname{kroneckerMap} f M N)$$$
Lean4
theorem kroneckerMap_reindex_left (f : α → β → γ) (el : l ≃ l') (em : m ≃ m') (M : Matrix l m α) (N : Matrix n n' β) :
kroneckerMap f (Matrix.reindex el em M) N =
reindex (el.prodCongr (Equiv.refl _)) (em.prodCongr (Equiv.refl _)) (kroneckerMap f M N) :=
kroneckerMap_reindex _ _ _ (Equiv.refl _) (Equiv.refl _) _ _
