derivedLength_zero — Mathlib

English

If I is solvable, then the derived length of I is 0 if and only if I is the zero ideal.

Русский

Если I разрешимо, то длина производной I равна 0 тогда и только тогда, когда I = {0}.

LaTeX

$$$\mathrm{derivedLengthOfIdeal}(R,L,I)=0 \iff I=\perp.$$$

Lean4

theorem derivedLength_zero (I : LieIdeal R L) [IsSolvable I] : derivedLengthOfIdeal R L I = 0 ↔ I = ⊥ :=
  by
  let s := {k | derivedSeriesOfIdeal R L k I = ⊥}
  change sInf s = 0 ↔ _
  have hne : s ≠ ∅ := by
    obtain ⟨k, hk⟩ := IsSolvable.solvable R I
    refine Set.Nonempty.ne_empty ⟨k, ?_⟩
    rw [derivedSeries_def, LieIdeal.derivedSeries_eq_bot_iff] at hk; exact hk
  simp [s, hne]

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