case pos
R : Type ?u.1133378
inst✝¹¹ : CommRing R
M : Type u_2
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.1133969
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.1134511
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e : Basis ι R M
A : Type ?u.1134989
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.1135487
inst✝² : Fintype κ
𝕜 : Type u_1
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
hf : ↑LinearMap.det f ≠ 1
H : ∃ s, Nonempty (Basis { x // x ∈ s } 𝕜 M)
⊢ FiniteDimensional 𝕜 M

case neg
R : Type ?u.1133378
inst✝¹¹ : CommRing R
M : Type u_2
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.1133969
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.1134511
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e : Basis ι R M
A : Type ?u.1134989
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.1135487
inst✝² : Fintype κ
𝕜 : Type u_1
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
hf : ↑LinearMap.det f ≠ 1
H : ¬∃ s, Nonempty (Basis { x // x ∈ s } 𝕜 M)
⊢ FiniteDimensional 𝕜 M
R : Type ?u.1133378
inst✝¹¹ : CommRing R
M : Type u_2
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.1133969
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.1134511
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e : Basis ι R M
A : Type ?u.1134989
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.1135487
inst✝² : Fintype κ
𝕜 : Type u_1
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
hf : ↑LinearMap.det f ≠ 1
⊢ FiniteDimensional 𝕜 M
by_cases H : ∃ s : Finset M, Nonempty (Basis s 𝕜 M)
case pos.intro.intro
R : Type ?u.1133378
inst✝¹¹ : CommRing R
M : Type u_2
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.1133969
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.1134511
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e : Basis ι R M
A : Type ?u.1134989
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.1135487
inst✝² : Fintype κ
𝕜 : Type u_1
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
hf : ↑LinearMap.det f ≠ 1
s : Finset M
hs : Basis { x // x ∈ s } 𝕜 M
⊢ FiniteDimensional 𝕜 M
case pos
R : Type ?u.1133378
inst✝¹¹ : CommRing R
M : Type u_2
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.1133969
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.1134511
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e : Basis ι R M
A : Type ?u.1134989
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.1135487
inst✝² : Fintype κ
𝕜 : Type u_1
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
hf : ↑LinearMap.det f ≠ 1
H : ∃ s, Nonempty (Basis { x // x ∈ s } 𝕜 M)
⊢ FiniteDimensional 𝕜 M
rcases H with ⟨s, ⟨hs⟩⟩
no goals
case pos.intro.intro
R : Type ?u.1133378
inst✝¹¹ : CommRing R
M : Type u_2
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.1133969
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.1134511
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e : Basis ι R M
A : Type ?u.1134989
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.1135487
inst✝² : Fintype κ
𝕜 : Type u_1
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
hf : ↑LinearMap.det f ≠ 1
s : Finset M
hs : Basis { x // x ∈ s } 𝕜 M
⊢ FiniteDimensional 𝕜 M
exact FiniteDimensional.of_fintype_basis hs
no goals
case neg
R : Type ?u.1133378
inst✝¹¹ : CommRing R
M : Type u_2
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.1133969
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.1134511
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e : Basis ι R M
A : Type ?u.1134989
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.1135487
inst✝² : Fintype κ
𝕜 : Type u_1
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
hf : ↑LinearMap.det f ≠ 1
H : ¬∃ s, Nonempty (Basis { x // x ∈ s } 𝕜 M)
⊢ FiniteDimensional 𝕜 M
classical simp [LinearMap.coe_det, H] at hf
no goals
case neg
R : Type ?u.1133378
inst✝¹¹ : CommRing R
M : Type u_2
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
M' : Type ?u.1133969
inst✝⁸ : AddCommGroup M'
inst✝⁷ : Module R M'
ι : Type ?u.1134511
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
e : Basis ι R M
A : Type ?u.1134989
inst✝⁴ : CommRing A
inst✝³ : Module A M
κ : Type ?u.1135487
inst✝² : Fintype κ
𝕜 : Type u_1
inst✝¹ : Field 𝕜
inst✝ : Module 𝕜 M
f : M →ₗ[𝕜] M
hf : ↑LinearMap.det f ≠ 1
H : ¬∃ s, Nonempty (Basis { x // x ∈ s } 𝕜 M)
⊢ FiniteDimensional 𝕜 M
simp [LinearMap.coe_det, H] at hf