reindexAlgEquiv_refl — Mathlib

English

Reindexing by the identity equivalence leaves the corresponding algebraic reindexing unchanged, i.e., reindexAlgEquiv R A (Equiv.refl m) = AlgEquiv.refl.

Русский

Реиндексация по тождественному эквиваленту сохраняет эквивалентность переноса: reindexAlgEquiv R A (Equiv.refl m) = AlgEquiv.refl.

LaTeX

$$$ \mathrm{reindexAlgEquiv}\ R\ A\ (\mathrm{Equiv.refl}\ m) = \mathrm{AlgEquiv.refl} $$$

Lean4

@[simp]
theorem reindexAlgEquiv_refl : reindexAlgEquiv R A (Equiv.refl m) = AlgEquiv.refl :=
  AlgEquiv.ext fun _ => rfl

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