no goals
R : Type u_1
inst✝⁷ : StrictOrderedCommRing R
M : Type u_3
N : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R N
ι : Type u_2
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : Nontrivial R
e : Basis ι R M
f : M ≃ₗ[R] N
⊢ Basis.orientation (Basis.map e f) = ↑(Orientation.map ι f) (Basis.orientation e)
simp_rw [Basis.orientation, Orientation.map_apply, Basis.det_map']