case mk.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
k : ℕ
hM : lowerCentralSeries R L M k = ⊥
⊢ ∃ k, ∀ (x : L), ↑(toEndomorphism R L M) x ^ k = 0
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
hM : IsNilpotent R L M
⊢ ∃ k, ∀ (x : L), ↑(toEndomorphism R L M) x ^ k = 0
obtain ⟨k, hM⟩ := hM
case mk.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
k : ℕ
hM : lowerCentralSeries R L M k = ⊥
⊢ ∀ (x : L), ↑(toEndomorphism R L M) x ^ k = 0
case mk.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
k : ℕ
hM : lowerCentralSeries R L M k = ⊥
⊢ ∃ k, ∀ (x : L), ↑(toEndomorphism R L M) x ^ k = 0
use k
case mk.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
k : ℕ
hM : lowerCentralSeries R L M k = ⊥
x : L
⊢ ↑(toEndomorphism R L M) x ^ k = 0
case mk.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
k : ℕ
hM : lowerCentralSeries R L M k = ⊥
⊢ ∀ (x : L), ↑(toEndomorphism R L M) x ^ k = 0
intro x
case mk.intro.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
k : ℕ
hM : lowerCentralSeries R L M k = ⊥
x : L
m : M
⊢ ↑(↑(toEndomorphism R L M) x ^ k) m = ↑0 m
case mk.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
k : ℕ
hM : lowerCentralSeries R L M k = ⊥
x : L
⊢ ↑(toEndomorphism R L M) x ^ k = 0
ext m
case mk.intro.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
k : ℕ
hM : lowerCentralSeries R L M k = ⊥
x : L
m : M
⊢ (↑(↑(toEndomorphism R L M) x)^[k]) m ∈ lowerCentralSeries R L M k
case mk.intro.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
k : ℕ
hM : lowerCentralSeries R L M k = ⊥
x : L
m : M
⊢ ↑(↑(toEndomorphism R L M) x ^ k) m = ↑0 m
rw [LinearMap.pow_apply, LinearMap.zero_apply, ← @LieSubmodule.mem_bot R L M, ← hM]
no goals
case mk.intro.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
k : ℕ
hM : lowerCentralSeries R L M k = ⊥
x : L
m : M
⊢ (↑(↑(toEndomorphism R L M) x)^[k]) m ∈ lowerCentralSeries R L M k
exact iterate_toEndomorphism_mem_lowerCentralSeries R L M x m k