hasTrivialRadical_iff_no_solvable_ideals

English

The radical is trivial if and only if every solvable ideal is zero.

Русский

Радикал тривиален тогда и только тогда, когда каждый разрешимый идеал равен нулю.

LaTeX

$$$(HasTrivialRadical\; R\; L) \iff (\forall I : LieIdeal\; R\; L, IsSolvable\ I \Rightarrow I = \bot)$$$

Lean4

theorem hasTrivialRadical_iff_no_solvable_ideals : HasTrivialRadical R L ↔ ∀ I : LieIdeal R L, IsSolvable I → I = ⊥ :=
  ⟨@HasTrivialRadical.eq_bot_of_isSolvable _ _ _ _ _, hasTrivialRadical_of_no_solvable_ideals⟩

Похожие утверждения