no goals
R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type ?u.2918948
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι : Type u_3
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
e : Basis ι R M
A : Type ?u.2919968
inst✝¹ : CommRing A
inst✝ : Module A M
w : ι → Rˣ
⊢ ↑(det e) ↑(unitsSMul e w) = ∏ i : ι, ↑(w i)
simp [Basis.det_apply]