R : Type ?u.1165630
inst✝¹¹ : CommRing R
M : Type u_2
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.1166221
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.1166763
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e : Basis ι R M
A : Type ?u.1167241
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.1167739
inst✝² : Fintype κ
𝕜 : Type u_1
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
hf : ↑LinearMap.det f = 0
this : FiniteDimensional 𝕜 M
⊢ range f < ⊤
R : Type ?u.1165630
inst✝¹¹ : CommRing R
M : Type u_2
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.1166221
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.1166763
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e : Basis ι R M
A : Type ?u.1167241
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.1167739
inst✝² : Fintype κ
𝕜 : Type u_1
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
hf : ↑LinearMap.det f = 0
⊢ range f < ⊤
have : FiniteDimensional 𝕜 M := by simp [f.finiteDimensional_of_det_ne_one, hf]
R : Type ?u.1165630
inst✝¹¹ : CommRing R
M : Type u_2
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.1166221
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.1166763
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e : Basis ι R M
A : Type ?u.1167241
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.1167739
inst✝² : Fintype κ
𝕜 : Type u_1
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
this : FiniteDimensional 𝕜 M
hf : ¬range f < ⊤
⊢ ¬↑LinearMap.det f = 0
R : Type ?u.1165630
inst✝¹¹ : CommRing R
M : Type u_2
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.1166221
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.1166763
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e : Basis ι R M
A : Type ?u.1167241
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.1167739
inst✝² : Fintype κ
𝕜 : Type u_1
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
hf : ↑LinearMap.det f = 0
this : FiniteDimensional 𝕜 M
⊢ range f < ⊤
contrapose hf
R : Type ?u.1165630
inst✝¹¹ : CommRing R
M : Type u_2
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.1166221
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.1166763
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e : Basis ι R M
A : Type ?u.1167241
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.1167739
inst✝² : Fintype κ
𝕜 : Type u_1
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
this : FiniteDimensional 𝕜 M
hf : IsUnit f
⊢ ¬↑LinearMap.det f = 0
R : Type ?u.1165630
inst✝¹¹ : CommRing R
M : Type u_2
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.1166221
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.1166763
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e : Basis ι R M
A : Type ?u.1167241
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.1167739
inst✝² : Fintype κ
𝕜 : Type u_1
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
this : FiniteDimensional 𝕜 M
hf : ¬range f < ⊤
⊢ ¬↑LinearMap.det f = 0
simp only [lt_top_iff_ne_top, Classical.not_not, ← isUnit_iff_range_eq_top] at hf
no goals
R : Type ?u.1165630
inst✝¹¹ : CommRing R
M : Type u_2
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.1166221
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.1166763
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e : Basis ι R M
A : Type ?u.1167241
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.1167739
inst✝² : Fintype κ
𝕜 : Type u_1
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
this : FiniteDimensional 𝕜 M
hf : IsUnit f
⊢ ¬↑LinearMap.det f = 0
exact isUnit_iff_ne_zero.1 (f.isUnit_det hf)
no goals
R : Type ?u.1165630
inst✝¹¹ : CommRing R
M : Type u_2
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.1166221
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.1166763
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e : Basis ι R M
A : Type ?u.1167241
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.1167739
inst✝² : Fintype κ
𝕜 : Type u_1
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
hf : ↑LinearMap.det f = 0
⊢ FiniteDimensional 𝕜 M
simp [f.finiteDimensional_of_det_ne_one, hf]