no goals
R : Type ?u.43313
inst✝¹⁰ : CommRing R
M : Type u_4
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
M' : Type ?u.43904
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
e : Basis ι R M
A : Type u_3
inst✝³ : CommRing A
inst✝² : Module A M
κ : Type u_1
inst✝¹ : Fintype κ
inst✝ : DecidableEq κ
b : Basis ι A M
c : Basis κ A M
f : M →ₗ[A] M
⊢ det (↑(toMatrix b b) f) = det (↑(toMatrix c c) f)
rw [← linearMap_toMatrix_mul_basis_toMatrix c b c, ← basis_toMatrix_mul_linearMap_toMatrix b c b,
    Matrix.det_conj_of_mul_eq_one] <;>
  rw [Basis.toMatrix_mul_toMatrix, Basis.toMatrix_self]