@[simp]

theorem LieIdeal.isSolvable_derivedSeriesOfIdeal_iff {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (n : ℕ) : LieAlgebra.IsSolvable ↥(LieAlgebra.derivedSeriesOfIdeal R L n I) ↔ LieAlgebra.IsSolvable ↥I

@[simp]

theorem LieIdeal.isSolvable_top_iff (R : Type u_2) (L : Type u_1) [CommRing R] [LieRing L] [LieAlgebra R L] : LieAlgebra.IsSolvable ↥⊤ ↔ LieAlgebra.IsSolvable L

theorem LieAlgebra.isSolvable_derivedSeries_iff (R : Type u_2) {L : Type u_1} [CommRing R] [LieRing L] [LieAlgebra R L] (n : ℕ) : IsSolvable ↥(derivedSeries R L n) ↔ IsSolvable L

theorem LieAlgebra.isSolvable_quotient_iff {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {I : LieIdeal R L} : IsSolvable (L ⧸ I) ↔ ∃ (k : ℕ), derivedSeries R L k ≤ I

theorem LieAlgebra.isSolvable_short_exact_iff {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : IsSolvable ↥I ∧ IsSolvable (L ⧸ I) ↔ IsSolvable L

@[simp]

theorem derivedAbelianOfIdeal_le_self {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : LieAlgebra.derivedAbelianOfIdeal I ≤ I