R : Type u_2
inst✝¹⁰ : CommRing R
M : Type u_1
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
M' : Type ?u.929764
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
ι : Type ?u.930306
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
e : Basis ι R M
A : Type ?u.930784
inst✝³ : CommRing A
inst✝² : Module A M
κ : Type ?u.931282
inst✝¹ : Fintype κ
inst✝ : Subsingleton M
f : M →ₗ[R] M
b : Basis (Fin 0) R M
⊢ ↑LinearMap.det f = 1
R : Type u_2
inst✝¹⁰ : CommRing R
M : Type u_1
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
M' : Type ?u.929764
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
ι : Type ?u.930306
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
e : Basis ι R M
A : Type ?u.930784
inst✝³ : CommRing A
inst✝² : Module A M
κ : Type ?u.931282
inst✝¹ : Fintype κ
inst✝ : Subsingleton M
f : M →ₗ[R] M
⊢ ↑LinearMap.det f = 1
have b : Basis (Fin 0) R M := Basis.empty M
R : Type u_2
inst✝¹⁰ : CommRing R
M : Type u_1
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
M' : Type ?u.929764
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
ι : Type ?u.930306
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
e : Basis ι R M
A : Type ?u.930784
inst✝³ : CommRing A
inst✝² : Module A M
κ : Type ?u.931282
inst✝¹ : Fintype κ
inst✝ : Subsingleton M
f : M →ₗ[R] M
b : Basis (Fin 0) R M
⊢ det (↑(toMatrix b b) f) = 1
R : Type u_2
inst✝¹⁰ : CommRing R
M : Type u_1
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
M' : Type ?u.929764
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
ι : Type ?u.930306
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
e : Basis ι R M
A : Type ?u.930784
inst✝³ : CommRing A
inst✝² : Module A M
κ : Type ?u.931282
inst✝¹ : Fintype κ
inst✝ : Subsingleton M
f : M →ₗ[R] M
b : Basis (Fin 0) R M
⊢ ↑LinearMap.det f = 1
rw [← f.det_toMatrix b]
no goals
R : Type u_2
inst✝¹⁰ : CommRing R
M : Type u_1
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
M' : Type ?u.929764
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
ι : Type ?u.930306
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
e : Basis ι R M
A : Type ?u.930784
inst✝³ : CommRing A
inst✝² : Module A M
κ : Type ?u.931282
inst✝¹ : Fintype κ
inst✝ : Subsingleton M
f : M →ₗ[R] M
b : Basis (Fin 0) R M
⊢ det (↑(toMatrix b b) f) = 1
exact Matrix.det_isEmpty