reindex_comp_tprod — Mathlib

English

Reindexing composes with the tprod via a canonical linear equivalence that permutes factors.

Русский

Переиндексация совместима с тprod через каноническое линейное эквивалентное отображение, переставляющее слагаемые.

LaTeX

$$$\\bigl(\\operatorname{reindex}_{R,R,s,e}\\bigr)\\circ \\operatorname{tprod}_R = \\operatorname{domDomCongrLinearEquiv'}^{\\,-1}_{R,R,s,e}(\\operatorname{tprod}_R).$$$

Lean4

@[simp]
theorem reindex_comp_tprod (e : ι ≃ ι₂) :
    (reindex R s e).compMultilinearMap (tprod R) = (domDomCongrLinearEquiv' R R s _ e).symm (tprod R) :=
  MultilinearMap.ext <| reindex_tprod e

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