map_comp_reindex_symm — Mathlib

English

A straightforward translation of map with reindexing expresses the same output as reindexed map.

Русский

Простая формулировка отображения с переиндексацией: вывод совпадает с переиндексированным отображением.

LaTeX

$$$\\operatorname{map} (f) \\circ \\operatorname{reindex}_{R,s,e} = \\operatorname{reindex}_{R,t,e} \\circ \\operatorname{map} f$$$

Lean4

theorem map_comp_reindex_symm (f : Π i, s i →ₗ[R] t i) (e : ι ≃ ι₂) :
    map f ∘ₗ (reindex R s e).symm = (reindex R t e).symm ∘ₗ map (fun i => f (e.symm i)) :=
  by
  ext m
  apply LinearEquiv.injective (reindex R t e)
  simp only [LinearMap.compMultilinearMap_apply, LinearMap.coe_comp, LinearEquiv.coe_coe, comp_apply, ← map_reindex,
    LinearEquiv.apply_symm_apply, map_tprod]

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