reindexAlgEquiv_symm — Mathlib

English

The inverse of the index relabelling AlgEquiv is the index relabelling corresponding to the inverse equivalence: (reindexAlgEquiv R A e).symm = reindexAlgEquiv R A e.symm.

Русский

Обратная к перераспределению индексов по AlgEquiv равна перераспределению по обратному эквиваленту: (reindexAlgEquiv R A e).symm = reindexAlgEquiv R A e.symm.

LaTeX

$$$ (\mathrm{reindexAlgEquiv}\ R\ A\ e).symm = \mathrm{reindexAlgEquiv}\ R\ A\ e\mathrm{.symm} $$$

Lean4

@[simp]
theorem reindexAlgEquiv_symm (e : m ≃ n) : (reindexAlgEquiv R A e).symm = reindexAlgEquiv R A e.symm :=
  rfl

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