reindex_neg — Mathlib

English

Reindexing respects negation: reindex e (−x) = − reindex e x.

Русский

Переиндексация сохраняет отрицание: reindex e (−x) = − reindex e x.

LaTeX

$$$\text{reindex_neg}: \; Orientation.reindex R M e (-x) = -Orientation.reindex R M e x.$$$

Lean4

@[simp]
protected theorem reindex_neg {ι ι' : Type*} (e : ι ≃ ι') (x : Orientation R M ι) :
    Orientation.reindex R M e (-x) = -Orientation.reindex R M e x :=
  Module.Ray.map_neg _ x

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