reindexLinearEquiv_trans — Mathlib

English

The composition of reindexLinearEquiv with itself corresponds to the transitive composition of the index equivalences.

Русский

Сочетание двух reindexLinearEquiv соответствует транспозиции индексов по композиции эквивалентностей.

LaTeX

$$$ (\mathrm{reindexLinearEquiv}\ R\ A e_1' e_2') \;\mathrm{trans} \; (\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_trans (e₁ : m ≃ m') (e₂ : n ≃ n') (e₁' : m' ≃ m'') (e₂' : n' ≃ n'') :
    (reindexLinearEquiv R A e₁ e₂).trans (reindexLinearEquiv R A e₁' e₂') =
      (reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂') : _ ≃ₗ[R] _) :=
  by
  ext
  rfl

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