reindex_refl — Mathlib

English

Reindexing by the identity is the identity orientation.

Русский

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

LaTeX

$$$\text{reindex_refl}: (Orientation.reindex R M (Equiv.refl ι)) = Equiv.refl _.$$$

Lean4

@[simp]
theorem reindex_refl : (Orientation.reindex R M <| Equiv.refl ι) = Equiv.refl _ := by
  rw [Orientation.reindex, AlternatingMap.domDomCongrₗ_refl, Module.Ray.map_refl]

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