orientation_reindex — Mathlib

English

The reindexed orientation equals the orientation of the reindexed basis.

Русский

Ориентация после переиндексации равна ориентации переразнесенной базы.

LaTeX

$$$\text{orientation_reindex}: (e.reindex ei).orientation = Orientation.reindex R M ei e.orientation$$$

Lean4

theorem orientation_reindex (e : Basis ι R M) (eι : ι ≃ ι') :
    (e.reindex eι).orientation = Orientation.reindex R M eι e.orientation := by
  simp_rw [Basis.orientation, Orientation.reindex_apply, Basis.det_reindex']

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