case h
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
m : M
⊢ (m ∈ ⨅ (x : L), Module.End.maximalGeneralizedEigenspace (↑(toEndomorphism R L M) x) 0) ↔ m ∈ ⊤
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
⊢ (⨅ (x : L), Module.End.maximalGeneralizedEigenspace (↑(toEndomorphism R L M) x) 0) = ⊤
ext m
case h
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
m : M
⊢ ∀ (i : L), ∃ k, ↑(↑(toEndomorphism R L M) i ^ k) m = 0
case h
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
m : M
⊢ (m ∈ ⨅ (x : L), Module.End.maximalGeneralizedEigenspace (↑(toEndomorphism R L M) x) 0) ↔ m ∈ ⊤
simp only [Module.End.mem_maximalGeneralizedEigenspace, Submodule.mem_top, sub_zero, iff_true_iff,
  zero_smul, Submodule.mem_iInf]
case h
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
m : M
x : L
⊢ ∃ k, ↑(↑(toEndomorphism R L M) x ^ k) m = 0
case h
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
m : M
⊢ ∀ (i : L), ∃ k, ↑(↑(toEndomorphism R L M) i ^ k) m = 0
intro x
case h.intro
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
m : M
x : L
k : ℕ
hk : ∀ (x : L), ↑(toEndomorphism R L M) x ^ k = 0
⊢ ∃ k, ↑(↑(toEndomorphism R L M) x ^ k) m = 0
case h
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
m : M
x : L
⊢ ∃ k, ↑(↑(toEndomorphism R L M) x ^ k) m = 0
obtain ⟨k, hk⟩ := nilpotent_endo_of_nilpotent_module R L M
case h.intro
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
m : M
x : L
k : ℕ
hk : ∀ (x : L), ↑(toEndomorphism R L M) x ^ k = 0
⊢ ↑(↑(toEndomorphism R L M) x ^ k) m = 0
case h.intro
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
m : M
x : L
k : ℕ
hk : ∀ (x : L), ↑(toEndomorphism R L M) x ^ k = 0
⊢ ∃ k, ↑(↑(toEndomorphism R L M) x ^ k) m = 0
use k
case h.intro
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
m : M
x : L
k : ℕ
hk : ∀ (x : L), ↑(toEndomorphism R L M) x ^ k = 0
⊢ ↑0 m = 0
case h.intro
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
m : M
x : L
k : ℕ
hk : ∀ (x : L), ↑(toEndomorphism R L M) x ^ k = 0
⊢ ↑(↑(toEndomorphism R L M) x ^ k) m = 0
rw [hk]
no goals
case h.intro
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
m : M
x : L
k : ℕ
hk : ∀ (x : L), ↑(toEndomorphism R L M) x ^ k = 0
⊢ ↑0 m = 0
exact LinearMap.zero_apply m