English
For two bases e1 and e2, their orientations are equal if and only if the determinant of e1 with respect to e2 is positive.
Русский
Ориентации двух базисов e1 и e2 равны тогда и только тогда, когда детерминант перехода от e2 к e1 положителен.
LaTeX
$$$$ e_1.{\\rm orientation} = e_2.{\\rm orientation} \\iff 0 < e_1.{\\rm det}\\,e_2 $$$$
Lean4
/-- The orientations given by two bases are equal if and only if the determinant of one basis
with respect to the other is positive. -/
theorem orientation_eq_iff_det_pos (e₁ e₂ : Basis ι R M) : e₁.orientation = e₂.orientation ↔ 0 < e₁.det e₂ :=
calc
e₁.orientation = e₂.orientation ↔ SameRay R e₁.det e₂.det := ray_eq_iff _ _
_ ↔ SameRay R (e₁.det e₂ • e₂.det) e₂.det := by rw [← e₁.det.eq_smul_basis_det e₂]
_ ↔ 0 < e₁.det e₂ := sameRay_smul_left_iff_of_ne e₂.det_ne_zero (e₁.isUnit_det e₂).ne_zero
