R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
⊢ IsLieAbelian { x // x ∈ ↑⊥ }
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
⊢ IsLieAbelian { x // x ∈ ↑(radical R L) }
rw [IsSemisimple.semisimple]
no goals
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
⊢ IsLieAbelian { x // x ∈ ↑⊥ }
exact isLieAbelian_bot R L