derivedSeriesOfIdeal_succ_le

Mathlib.Algebra.Lie.Solvable

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

English

The derived series is monotone with respect to inclusion of ideals: if I ≤ J then D k I ≤ D k J for all k.

Русский

Производные ряды монотонны по включениям: если I ≤ J, то D_k I ≤ D_k J для всех k.

LaTeX

$$$D(k)I \le D(k)J \quad \text{whenever } I \le J$$$

Lean4

theorem derivedSeriesOfIdeal_succ_le (k : ℕ) : D (k + 1) I ≤ D k I :=
  derivedSeriesOfIdeal_le (le_refl I) k.le_succ

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

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

Разделы

Аффилиация

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