kroneckerMap_reindex_right — Mathlib

English

If en is an index equivalence on n, then kroneckerMap f M (reindex en en N) equals reindex ... (kroneckerMap f M N).

Русский

Пусть en — эквивалент индексов на n; тогда kroneckerMap f M (reindex en en N) эквивалентно reindex ... (kroneckerMap f M N).

LaTeX

$$$\operatorname{kroneckerMap} f M (\mathrm{reindex} en ep N) = \mathrm{reindex} ((\mathrm{Equiv.refl _}).prodCongr en) ((\mathrm{Equiv.refl _}).prodCongr ep) (\operatorname{kroneckerMap} f M N)$$$

Lean4

theorem kroneckerMap_reindex_right (f : α → β → γ) (em : m ≃ m') (en : n ≃ n') (M : Matrix l l' α) (N : Matrix m n β) :
    kroneckerMap f M (reindex em en N) =
      reindex ((Equiv.refl _).prodCongr em) ((Equiv.refl _).prodCongr en) (kroneckerMap f M N) :=
  kroneckerMap_reindex _ (Equiv.refl _) (Equiv.refl _) _ _ _ _

Похожие утверждения