R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : ∀ (I : LieIdeal R L), IsLieAbelian { x // x ∈ ↑I } → I = ⊥
⊢ center R L = ⊥
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : IsSemisimple R L
⊢ center R L = ⊥
rw [isSemisimple_iff_no_abelian_ideals] at h
case a
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : ∀ (I : LieIdeal R L), IsLieAbelian { x // x ∈ ↑I } → I = ⊥
⊢ IsLieAbelian { x // x ∈ ↑(center R L) }
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : ∀ (I : LieIdeal R L), IsLieAbelian { x // x ∈ ↑I } → I = ⊥
⊢ center R L = ⊥
apply h
no goals
case a
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
h : ∀ (I : LieIdeal R L), IsLieAbelian { x // x ∈ ↑I } → I = ⊥
⊢ IsLieAbelian { x // x ∈ ↑(center R L) }
infer_instance