English
The determinant of the adjusted basis equals the determinant of the original basis up to a possible sign flip.
Русский
Детерминант откорректированного базиса равен детерминанту исходного базиса с возможным знаком.
LaTeX
$$$$ (e.{\\rm adjustToOrientation} x).{\\rm det} = e.{\\rm det} \\quad\\lor\\quad (e.{\\rm adjustToOrientation} x).{\\rm det} = -e.{\\rm det} $$$$
Lean4
theorem det_adjustToOrientation [Nonempty ι] (e : Basis ι R M) (x : Orientation R M ι) :
(e.adjustToOrientation x).det = e.det ∨ (e.adjustToOrientation x).det = -e.det :=
by
dsimp [Basis.adjustToOrientation]
split_ifs
· left
rfl
· right
simp only [e.det_unitsSMul, Finset.mem_univ, Finset.prod_update_of_mem, Pi.one_apply, Finset.prod_const_one,
mul_one, inv_neg, inv_one, Units.val_neg, Units.val_one]
ext
simp
