no goals
R : Type ?u.143873
inst✝¹¹ : CommRing R
M : Type u_2
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.144464
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e : Basis ι R M
A : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.145982
inst✝² : Fintype κ
ι' : Type u_1
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
tb : Trunc (Basis ι A M)
b' : Basis ι' A M
f : M →ₗ[A] M
⊢ ↑(detAux tb) f = det (↑(toMatrix b' b') f)
induction tb using Trunc.induction_on with
| h b => rw [detAux_def', det_toMatrix_eq_det_toMatrix b b']
no goals
case h
R : Type ?u.143873
inst✝¹¹ : CommRing R
M : Type u_2
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.144464
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type u_4
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e : Basis ι R M
A : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.145982
inst✝² : Fintype κ
ι' : Type u_1
inst✝¹ : Fintype ι'
inst✝ : DecidableEq ι'
b' : Basis ι' A M
f : M →ₗ[A] M
b : Basis ι A M
⊢ ↑(detAux (Trunc.mk b)) f = det (↑(toMatrix b' b') f)
rw [detAux_def', det_toMatrix_eq_det_toMatrix b b']