R : Type u_1
inst✝⁷ : StrictOrderedCommRing R
M : Type u_3
N : Type ?u.98544
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
w : ι → Rˣ
⊢ SameRay R (det (unitsSMul e w)) ((↑(∏ i : ι, w i)⁻¹ * ∏ i : ι, ↑(w i)) • det (unitsSMul e w))
R : Type u_1
inst✝⁷ : StrictOrderedCommRing R
M : Type u_3
N : Type ?u.98544
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
w : ι → Rˣ
⊢ Basis.orientation (unitsSMul e w) = (∏ i : ι, w i)⁻¹ • Basis.orientation e
rw [Basis.orientation, Basis.orientation, smul_rayOfNeZero, ray_eq_iff,
  e.det.eq_smul_basis_det (e.unitsSMul w), det_unitsSMul_self, Units.smul_def, smul_smul]
R : Type u_1
inst✝⁷ : StrictOrderedCommRing R
M : Type u_3
N : Type ?u.98544
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
w : ι → Rˣ
⊢ SameRay R (det (unitsSMul e w)) (↑((∏ i : ι, w i)⁻¹ * ∏ i : ι, w i) • det (unitsSMul e w))
R : Type u_1
inst✝⁷ : StrictOrderedCommRing R
M : Type u_3
N : Type ?u.98544
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
w : ι → Rˣ
⊢ SameRay R (det (unitsSMul e w)) ((↑(∏ i : ι, w i)⁻¹ * ∏ i : ι, ↑(w i)) • det (unitsSMul e w))
norm_cast
R : Type u_1
inst✝⁷ : StrictOrderedCommRing R
M : Type u_3
N : Type ?u.98544
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
w : ι → Rˣ
⊢ SameRay R (det (unitsSMul e w)) (det (unitsSMul e w))
R : Type u_1
inst✝⁷ : StrictOrderedCommRing R
M : Type u_3
N : Type ?u.98544
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
w : ι → Rˣ
⊢ SameRay R (det (unitsSMul e w)) (↑((∏ i : ι, w i)⁻¹ * ∏ i : ι, w i) • det (unitsSMul e w))
simp
no goals
R : Type u_1
inst✝⁷ : StrictOrderedCommRing R
M : Type u_3
N : Type ?u.98544
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
w : ι → Rˣ
⊢ SameRay R (det (unitsSMul e w)) (det (unitsSMul e w))
exact SameRay.rfl