R : Type ?u.99440
inst✝⁹ : CommRing R
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M' : Type ?u.100031
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.101549
inst✝ : Fintype κ
b : Basis ι A M
f : M →ₗ[A] M
⊢ ↑(Trunc.lift (fun b => MonoidHom.comp detMonoidHom ↑(toMatrixAlgEquiv b))
          (_ :
            ∀ (b c : Basis ι A M),
              (fun b => MonoidHom.comp detMonoidHom ↑(toMatrixAlgEquiv b)) b =
                (fun b => MonoidHom.comp detMonoidHom ↑(toMatrixAlgEquiv b)) c)
          (Trunc.mk b))
      f =
    det (↑(toMatrix b b) f)
R : Type ?u.99440
inst✝⁹ : CommRing R
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M' : Type ?u.100031
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.101549
inst✝ : Fintype κ
b : Basis ι A M
f : M →ₗ[A] M
⊢ ↑(detAux (Trunc.mk b)) f = det (↑(toMatrix b b) f)
rw [detAux]
no goals
R : Type ?u.99440
inst✝⁹ : CommRing R
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M' : Type ?u.100031
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.101549
inst✝ : Fintype κ
b : Basis ι A M
f : M →ₗ[A] M
⊢ ↑(Trunc.lift (fun b => MonoidHom.comp detMonoidHom ↑(toMatrixAlgEquiv b))
          (_ :
            ∀ (b c : Basis ι A M),
              (fun b => MonoidHom.comp detMonoidHom ↑(toMatrixAlgEquiv b)) b =
                (fun b => MonoidHom.comp detMonoidHom ↑(toMatrixAlgEquiv b)) c)
          (Trunc.mk b))
      f =
    det (↑(toMatrix b b) f)
rfl