abelian_iff_derived_one_eq_bot — Mathlib

English

An ideal I is Lie abelian iff its first derived series is zero: IsLieAbelian I ↔ D_1 I = ⊥.

Русский

Идеал I является абелевым относитательно Ли эквивалентно тому, что первый производный ряд равен нулю: IsLieAbelian I ⇔ D_1 I = ⊥.

LaTeX

$$$IsLieAbelian(I) \iff D(1)I = \bot$$$

Lean4

theorem abelian_iff_derived_one_eq_bot : IsLieAbelian I ↔ derivedSeriesOfIdeal R L 1 I = ⊥ := by
  rw [derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_zero, LieSubmodule.lie_abelian_iff_lie_self_eq_bot]

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