case h
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
f : M ≃ₗ[R] M'
v : Basis ι R M
v' : Basis ι R M'
⊢ ?B ⬝ ↑(toMatrix v v') ↑f = 1

case B
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
f : M ≃ₗ[R] M'
v : Basis ι R M
v' : Basis ι R M'
⊢ Matrix ι ι R
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
f : M ≃ₗ[R] M'
v : Basis ι R M
v' : Basis ι R M'
⊢ IsUnit (det (↑(toMatrix v v') ↑f))
apply isUnit_det_of_left_inverse
no goals
case h
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
f : M ≃ₗ[R] M'
v : Basis ι R M
v' : Basis ι R M'
⊢ ?B ⬝ ↑(toMatrix v v') ↑f = 1

case B
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
f : M ≃ₗ[R] M'
v : Basis ι R M
v' : Basis ι R M'
⊢ Matrix ι ι R
simpa using (LinearMap.toMatrix_comp v v' v f.symm f).symm