no goals
R : Type u_2
inst✝⁴ : LinearOrderedCommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e₁ e₂ : Basis ι R M
⊢ SameRay R (det e₁) (det e₂) ↔ SameRay R (↑(det e₁) ↑e₂ • det e₂) (det e₂)
rw [← e₁.det.eq_smul_basis_det e₂]