R : Type ?u.1194769
inst✝¹¹ : CommRing R
M : Type u_2
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.1195360
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.1195902
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e : Basis ι R M
A : Type ?u.1196380
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.1196878
inst✝² : Fintype κ
𝕜 : Type u_1
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
hf : ↑LinearMap.det f = 0
this : FiniteDimensional 𝕜 M
⊢ ⊥ < ker f
R : Type ?u.1194769
inst✝¹¹ : CommRing R
M : Type u_2
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.1195360
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.1195902
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e : Basis ι R M
A : Type ?u.1196380
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.1196878
inst✝² : Fintype κ
𝕜 : Type u_1
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
hf : ↑LinearMap.det f = 0
⊢ ⊥ < ker f
have : FiniteDimensional 𝕜 M := by simp [f.finiteDimensional_of_det_ne_one, hf]
R : Type ?u.1194769
inst✝¹¹ : CommRing R
M : Type u_2
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.1195360
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.1195902
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e : Basis ι R M
A : Type ?u.1196380
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.1196878
inst✝² : Fintype κ
𝕜 : Type u_1
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
this : FiniteDimensional 𝕜 M
hf : ¬⊥ < ker f
⊢ ¬↑LinearMap.det f = 0
R : Type ?u.1194769
inst✝¹¹ : CommRing R
M : Type u_2
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.1195360
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.1195902
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e : Basis ι R M
A : Type ?u.1196380
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.1196878
inst✝² : Fintype κ
𝕜 : Type u_1
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
hf : ↑LinearMap.det f = 0
this : FiniteDimensional 𝕜 M
⊢ ⊥ < ker f
contrapose hf
R : Type ?u.1194769
inst✝¹¹ : CommRing R
M : Type u_2
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.1195360
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.1195902
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e : Basis ι R M
A : Type ?u.1196380
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.1196878
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.1194769
inst✝¹¹ : CommRing R
M : Type u_2
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.1195360
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.1195902
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e : Basis ι R M
A : Type ?u.1196380
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.1196878
inst✝² : Fintype κ
𝕜 : Type u_1
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
this : FiniteDimensional 𝕜 M
hf : ¬⊥ < ker f
⊢ ¬↑LinearMap.det f = 0
simp only [bot_lt_iff_ne_bot, Classical.not_not, ← isUnit_iff_ker_eq_bot] at hf
no goals
R : Type ?u.1194769
inst✝¹¹ : CommRing R
M : Type u_2
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.1195360
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.1195902
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e : Basis ι R M
A : Type ?u.1196380
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.1196878
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.1194769
inst✝¹¹ : CommRing R
M : Type u_2
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.1195360
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.1195902
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e : Basis ι R M
A : Type ?u.1196380
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.1196878
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]