no goals
R : Type u_1
inst✝⁶ : LinearOrderedCommRing R
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Nontrivial R
inst✝ : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
v : ι → M
⊢ abs (↑(det (adjustToOrientation e x)) v) = abs (↑(det e) v)
cases' e.det_adjustToOrientation x with h h <;> simp [h]