case intro
R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Algebra R A
L : Type v
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
x : { x // x ∈ K }
n : ℕ
hn : ↑(LieAlgebra.ad R L) ↑x ^ n = 0
⊢ IsNilpotent (↑(LieAlgebra.ad R { x // x ∈ K }) x)
R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Algebra R A
L : Type v
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
x : { x // x ∈ K }
h : IsNilpotent (↑(LieAlgebra.ad R L) ↑x)
⊢ IsNilpotent (↑(LieAlgebra.ad R { x // x ∈ K }) x)
obtain ⟨n, hn⟩ := h
case intro
R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Algebra R A
L : Type v
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
x : { x // x ∈ K }
n : ℕ
hn : ↑(LieAlgebra.ad R L) ↑x ^ n = 0
⊢ ↑(LieAlgebra.ad R { x // x ∈ K }) x ^ n = 0
case intro
R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Algebra R A
L : Type v
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
x : { x // x ∈ K }
n : ℕ
hn : ↑(LieAlgebra.ad R L) ↑x ^ n = 0
⊢ IsNilpotent (↑(LieAlgebra.ad R { x // x ∈ K }) x)
use n
no goals
case intro
R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Algebra R A
L : Type v
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
x : { x // x ∈ K }
n : ℕ
hn : ↑(LieAlgebra.ad R L) ↑x ^ n = 0
⊢ ↑(LieAlgebra.ad R { x // x ∈ K }) x ^ n = 0
exact LinearMap.submodule_pow_eq_zero_of_pow_eq_zero (K.ad_comp_incl_eq x) hn