reindex_reindex — Mathlib

English

Reindexing with the identity map is the identity on the PiTensorProduct.

Русский

Переиндексация по тождественному отображению есть тождественное отображение на PiTensorProduct.

LaTeX

$$$\\operatorname{reindex}_{R,s}(\\operatorname{Equiv.refl}\\, \\iota) = \\operatorname{LinearEquiv.refl}_{R} $$$

Lean4

theorem reindex_reindex (e : ι ≃ ι₂) (e' : ι₂ ≃ ι₃) (x : ⨂[R] i, s i) :
    reindex R _ e' (reindex R s e x) = reindex R s (e.trans e') x :=
  LinearEquiv.congr_fun (reindex_trans e e' : _ = reindex R s (e.trans e')) x

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