map_of_isEmpty — Mathlib

English

Orientation map commutes with negation: map ι f (−x) = − map ι f x.

Русский

Отображение ориентации сохраняет операцию отрицания: map ι f (−x) = − map ι f x.

LaTeX

$$$\text{map_neg}: \; \text{Orientation.map } ι f (-x) = -\text{Orientation.map } ι f x$$$

Lean4

@[simp]
theorem map_of_isEmpty [IsEmpty ι] (x : Orientation R M ι) (f : M ≃ₗ[R] M) : Orientation.map ι f x = x := by
  induction x using Module.Ray.ind with
  | h g hg =>
    rw [Orientation.map_apply]
    congr
    ext i
    rw [AlternatingMap.compLinearMap_apply]
    congr
    simp only [LinearEquiv.coe_coe, eq_iff_true_of_subsingleton]

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