theorem LieIdeal.radical_quotient_eq_of_isSolvable {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) [LieAlgebra.IsSolvable ↥I] : LieAlgebra.radical R (L ⧸ I) = map (Quotient.mk' I) (LieAlgebra.radical R L)

@[simp]

theorem LieAlgebra.map_equiv_radical {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (e : L ≃ₗ⁅R⁆ L₂) : LieIdeal.map e.toLieHom (radical R L) = radical R L₂

theorem LieEquiv.hasTrivialRadical_iff_equiv_hasTrivialRadical {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (e : L ≃ₗ⁅R⁆ L₂) : LieAlgebra.HasTrivialRadical R L ↔ LieAlgebra.HasTrivialRadical R L₂

instance instHasTrivialRadicalQuotientLieIdealRadicalOfIsNoetherian_ado {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] [IsNoetherian R L] : LieAlgebra.HasTrivialRadical R (L ⧸ LieAlgebra.radical R L)