abelian_of_solvable_ideal_eq_bot_iff

English

For a solvable ideal I, derivedAbelianOfIdeal(I) equals zero iff I equals zero; otherwise it is nonzero.

Русский

Для разрешимого идеала I: derivedAbelianOfIdeal(I)=0 тогда и только тогда, когда I=0; иначе ненулевой.

LaTeX

$$$\mathrm{derivedAbelianOfIdeal}(I) = 0 \iff I=0.$$$

Lean4

theorem abelian_of_solvable_ideal_eq_bot_iff (I : LieIdeal R L) [h : IsSolvable I] :
    derivedAbelianOfIdeal I = ⊥ ↔ I = ⊥ :=
  by
  dsimp only [derivedAbelianOfIdeal]
  split
  · simp_all only [derivedLength_zero]
  · rename_i k h
    obtain ⟨_, h₂⟩ := (derivedSeries_of_derivedLength_succ R L I k).mp h
    have h₃ : I ≠ ⊥ := by rintro rfl; apply h₂; apply derivedSeries_of_bot_eq_bot
    simp only [h₂, h₃]

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