reindexLinearEquiv_comp — Mathlib

English

The composition of two reindexLinearEquiv maps equals the reindexLinearEquiv map for the composed index equivalences.

Русский

Составление двух reindexLinearEquiv даёт reindexLinearEquiv для композиции индексов.

LaTeX

$$$ (\mathrm{reindexLinearEquiv}\ R\ A e_1' e_2') \circ (\mathrm{reindexLinearEquiv}\ R\ A e_1 e_2) = \mathrm{reindexLinearEquiv}\ R\ A (e_1.\mathrm{trans} e_1') (e_2.\mathrm{trans} e_2'). $$$

Lean4

theorem reindexLinearEquiv_comp (e₁ : m ≃ m') (e₂ : n ≃ n') (e₁' : m' ≃ m'') (e₂' : n' ≃ n'') :
    reindexLinearEquiv R A e₁' e₂' ∘ reindexLinearEquiv R A e₁ e₂ =
      reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂') :=
  by
  rw [← reindexLinearEquiv_trans]
  rfl

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