map_refl — Mathlib

English

Mapping with the identity linear equivalence yields the identity orientation.

Русский

Отображение через тождественный линейный эквалент сохраняет ориентирование.

LaTeX

$$$\text{map_refl}: \; Orientation.map ι (LinearEquiv.refl R M) = Equiv.refl (Orientation R M ι).$$$

Lean4

@[simp]
theorem map_refl : (Orientation.map ι <| LinearEquiv.refl R M) = Equiv.refl _ := by
  rw [Orientation.map, AlternatingMap.domLCongr_refl, Module.Ray.map_refl]

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