English
Negating a single basis vector (via units_smul) negates the orientation of the basis.
Русский
Непосредственно повторяется утверждение о том, что отрицание одного вектора базиса меняет ориентацию на противоположную.
LaTeX
$$$$ (e.{\\rm unitsSMul}(\\mathrm{update}\\,1\\,i\\,(-1))).{\\rm orientation} = -e.{\\rm orientation} $$$$
Lean4
/-- Given a basis and an orientation, return a basis giving that orientation: either the original
basis, or one constructed by negating a single (arbitrary) basis vector. -/
def adjustToOrientation [Nonempty ι] (e : Basis ι R M) (x : Orientation R M ι) : Basis ι R M :=
haveI := Classical.decEq (Orientation R M ι)
if e.orientation = x then e else e.unitsSMul (Function.update 1 (Classical.arbitrary ι) (-1))
