R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
h : ⊥ = ⊤
⊢ Subsingleton L
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
h : IsLieAbelian L
⊢ Subsingleton L
rw [isLieAbelian_iff_center_eq_top R L, center_eq_bot_of_semisimple] at h
no goals
R : Type u
L : Type v
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
inst✝ : IsSemisimple R L
h : ⊥ = ⊤
⊢ Subsingleton L
exact (LieSubmodule.subsingleton_iff R L L).mp (subsingleton_of_bot_eq_top h)