R : Type ?u.421389
inst✝⁹ : CommRing R
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M' : Type ?u.421980
inst✝⁶ : AddCommGroup M'
inst✝⁵ : Module R M'
ι : Type u_1
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
e : Basis ι R M
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Module A M
κ : Type ?u.423498
inst✝ : Fintype κ
b : Basis ι A M
f : M →ₗ[A] M
this : DecidableEq M
⊢ det (↑(toMatrix b b) f) = ↑LinearMap.det f
R : Type ?u.421389
inst✝⁹ : CommRing R
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M' : Type ?u.421980
inst✝⁶ : AddCommGroup M'
inst✝⁵ : Module R M'
ι : Type u_1
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
e : Basis ι R M
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Module A M
κ : Type ?u.423498
inst✝ : Fintype κ
b : Basis ι A M
f : M →ₗ[A] M
⊢ det (↑(toMatrix b b) f) = ↑LinearMap.det f
haveI := Classical.decEq M
R : Type ?u.421389
inst✝⁹ : CommRing R
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M' : Type ?u.421980
inst✝⁶ : AddCommGroup M'
inst✝⁵ : Module R M'
ι : Type u_1
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
e : Basis ι R M
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Module A M
κ : Type ?u.423498
inst✝ : Fintype κ
b : Basis ι A M
f : M →ₗ[A] M
this : DecidableEq M
⊢ det (↑(toMatrix b b) f) = det (↑(toMatrix (Basis.reindexFinsetRange b) (Basis.reindexFinsetRange b)) f)
R : Type ?u.421389
inst✝⁹ : CommRing R
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M' : Type ?u.421980
inst✝⁶ : AddCommGroup M'
inst✝⁵ : Module R M'
ι : Type u_1
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
e : Basis ι R M
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Module A M
κ : Type ?u.423498
inst✝ : Fintype κ
b : Basis ι A M
f : M →ₗ[A] M
this : DecidableEq M
⊢ det (↑(toMatrix b b) f) = ↑LinearMap.det f
rw [det_eq_det_toMatrix_of_finset b.reindexFinsetRange]
no goals
R : Type ?u.421389
inst✝⁹ : CommRing R
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M' : Type ?u.421980
inst✝⁶ : AddCommGroup M'
inst✝⁵ : Module R M'
ι : Type u_1
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
e : Basis ι R M
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Module A M
κ : Type ?u.423498
inst✝ : Fintype κ
b : Basis ι A M
f : M →ₗ[A] M
this : DecidableEq M
⊢ det (↑(toMatrix b b) f) = det (↑(toMatrix (Basis.reindexFinsetRange b) (Basis.reindexFinsetRange b)) f)
apply det_toMatrix_eq_det_toMatrix b