reindex_trans — Mathlib

English

Reindexing composes associatively: reindex e then reindex e' equals reindex (e then e').

Русский

Переиндексация по цепочке отображений ассоциативна: переиндексация по e затем по e' равна переиндексации по композиции.

LaTeX

$$$(\\operatorname{reindex}_{R,s,e}).trans (\\operatorname{reindex}_{R, (\\lambda k. s (e^{-1}(k))), e'}) = \\operatorname{reindex}_{R,s, e \\circ e'}$$$

Lean4

@[simp]
theorem reindex_trans (e : ι ≃ ι₂) (e' : ι₂ ≃ ι₃) : (reindex R s e).trans (reindex R _ e') = reindex R s (e.trans e') :=
  by
  apply LinearEquiv.toLinearMap_injective
  ext f
  simp only [LinearEquiv.trans_apply, LinearEquiv.coe_coe, reindex_tprod, LinearMap.coe_compMultilinearMap,
    Function.comp_apply, reindex_comp_tprod]
  congr

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