abelian_derivedAbelianOfIdeal — Mathlib

English

For any Lie ideal I, the derivedAbelianOfIdeal(I) is abelian.

Русский

Для любого идеала I производнаяAbelianOfIdeal(I) абелева.

LaTeX

$$$\text{IsLieAbelian}(\mathrm{derivedAbelianOfIdeal}(I)).$$$

Lean4

theorem abelian_derivedAbelianOfIdeal (I : LieIdeal R L) : IsLieAbelian (derivedAbelianOfIdeal I) :=
  by
  dsimp only [derivedAbelianOfIdeal]
  rcases h : derivedLengthOfIdeal R L I with - | k
  · dsimp; infer_instance
  · rw [derivedSeries_of_derivedLength_succ] at h; exact h.1

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