case H
R : Type u_2
inst✝⁸ : CommRing R
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type ?u.2761525
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
e✝ : Basis ι R M
A : Type ?u.2762545
inst✝¹ : CommRing A
inst✝ : Module A M
e : Basis ι R M
w : ι → Rˣ
f : ι → M
⊢ ↑(det (unitsSMul e w)) f = ↑(↑(∏ i : ι, w i)⁻¹ • det e) f
R : Type u_2
inst✝⁸ : CommRing R
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type ?u.2761525
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
e✝ : Basis ι R M
A : Type ?u.2762545
inst✝¹ : CommRing A
inst✝ : Module A M
e : Basis ι R M
w : ι → Rˣ
⊢ det (unitsSMul e w) = ↑(∏ i : ι, w i)⁻¹ • det e
ext f
case H
R : Type u_2
inst✝⁸ : CommRing R
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type ?u.2761525
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
e✝ : Basis ι R M
A : Type ?u.2762545
inst✝¹ : CommRing A
inst✝ : Module A M
e : Basis ι R M
w : ι → Rˣ
f : ι → M
⊢ (Matrix.det fun i j => ↑(↑(unitsSMul e w).repr (f j)) i) =
    ↑(∏ i : ι, w i)⁻¹ • Matrix.det fun i j => ↑(↑e.repr (f j)) i
case H
R : Type u_2
inst✝⁸ : CommRing R
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type ?u.2761525
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
e✝ : Basis ι R M
A : Type ?u.2762545
inst✝¹ : CommRing A
inst✝ : Module A M
e : Basis ι R M
w : ι → Rˣ
f : ι → M
⊢ ↑(det (unitsSMul e w)) f = ↑(↑(∏ i : ι, w i)⁻¹ • det e) f
change
  (Matrix.det fun i j => (e.unitsSMul w).repr (f j) i) =
    (↑(∏ i, w i)⁻¹ : R) • Matrix.det fun i j => e.repr (f j) i
case H
R : Type u_2
inst✝⁸ : CommRing R
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type ?u.2761525
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
e✝ : Basis ι R M
A : Type ?u.2762545
inst✝¹ : CommRing A
inst✝ : Module A M
e : Basis ι R M
w : ι → Rˣ
f : ι → M
⊢ (Matrix.det fun i j => (w i)⁻¹ • ↑(↑e.repr (f j)) i) = ↑(∏ i : ι, w i)⁻¹ • Matrix.det fun i j => ↑(↑e.repr (f j)) i
case H
R : Type u_2
inst✝⁸ : CommRing R
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type ?u.2761525
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
e✝ : Basis ι R M
A : Type ?u.2762545
inst✝¹ : CommRing A
inst✝ : Module A M
e : Basis ι R M
w : ι → Rˣ
f : ι → M
⊢ (Matrix.det fun i j => ↑(↑(unitsSMul e w).repr (f j)) i) =
    ↑(∏ i : ι, w i)⁻¹ • Matrix.det fun i j => ↑(↑e.repr (f j)) i
simp only [e.repr_unitsSMul]
case h.e'_3.h.e'_1
R : Type u_2
inst✝⁸ : CommRing R
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type ?u.2761525
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
e✝ : Basis ι R M
A : Type ?u.2762545
inst✝¹ : CommRing A
inst✝ : Module A M
e : Basis ι R M
w : ι → Rˣ
f : ι → M
⊢ ↑(∏ i : ι, w i)⁻¹ = ∏ i : ι, ↑(w i)⁻¹
case H
R : Type u_2
inst✝⁸ : CommRing R
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type ?u.2761525
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
e✝ : Basis ι R M
A : Type ?u.2762545
inst✝¹ : CommRing A
inst✝ : Module A M
e : Basis ι R M
w : ι → Rˣ
f : ι → M
⊢ (Matrix.det fun i j => (w i)⁻¹ • ↑(↑e.repr (f j)) i) = ↑(∏ i : ι, w i)⁻¹ • Matrix.det fun i j => ↑(↑e.repr (f j)) i
convert Matrix.det_mul_column (fun i => (↑(w i)⁻¹ : R)) fun i j => e.repr (f j) i
case h.e'_3.h.e'_1
R : Type u_2
inst✝⁸ : CommRing R
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type ?u.2761525
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
e✝ : Basis ι R M
A : Type ?u.2762545
inst✝¹ : CommRing A
inst✝ : Module A M
e : Basis ι R M
w : ι → Rˣ
f : ι → M
⊢ ↑(∏ x : ι, (w x)⁻¹) = ∏ i : ι, ↑(w i)⁻¹
case h.e'_3.h.e'_1
R : Type u_2
inst✝⁸ : CommRing R
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type ?u.2761525
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
e✝ : Basis ι R M
A : Type ?u.2762545
inst✝¹ : CommRing A
inst✝ : Module A M
e : Basis ι R M
w : ι → Rˣ
f : ι → M
⊢ ↑(∏ i : ι, w i)⁻¹ = ∏ i : ι, ↑(w i)⁻¹
simp only [← Finset.prod_inv_distrib]
no goals
case h.e'_3.h.e'_1
R : Type u_2
inst✝⁸ : CommRing R
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
M' : Type ?u.2761525
inst✝⁵ : AddCommGroup M'
inst✝⁴ : Module R M'
ι : Type u_1
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
e✝ : Basis ι R M
A : Type ?u.2762545
inst✝¹ : CommRing A
inst✝ : Module A M
e : Basis ι R M
w : ι → Rˣ
f : ι → M
⊢ ↑(∏ x : ι, (w x)⁻¹) = ∏ i : ι, ↑(w i)⁻¹
norm_cast