orientation — Mathlib

English

The orientation associated to a basis via orientation_map corresponds to the map of orientation under a given linear equivalence.

Русский

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

LaTeX

$$$\text{orientation_map}: (e.map f).orientation = Orientation.map \; ι\; f \; e.orientation$$$

Lean4

/-- The orientation given by a basis. -/
protected def orientation (e : Basis ι R M) : Orientation R M ι :=
  rayOfNeZero R _ e.det_ne_zero

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