derivedSeriesOfIdeal_antitone

Mathlib.Algebra.Lie.Solvable

URI: https://scilib.ai/kg/mathlib#LieAlgebra.derivedSeriesOfIdeal_antitone

English

Several standard equalities for derived series hold, including D(0) = I and D(k+1) = [D(k), D(k)].

Русский

Стандартные равенства для производных рядов: D(0) = I и D(k+1) = [D(k), D(k)].

LaTeX

$$$D(0)I = I\quad\text{and}\quad D(k+1)I = [D(k)I, D(k)I]$$$

Lean4

theorem derivedSeriesOfIdeal_antitone {k l : ℕ} (h : l ≤ k) : D k I ≤ D l I :=
  derivedSeriesOfIdeal_le (le_refl I) h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru