derivedSeriesOfIdeal_mono

Mathlib.Algebra.Lie.Solvable

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

English

The derived series of any ideal with the zero step yields the zero ideal: D k ⊥ = ⊥.

Русский

Производный ряд любого идеала на нулевом шаге равен нулю: D_k ⊥ = ⊥.

LaTeX

$$$D(k)\,\bot = \bot$$$

Lean4

theorem derivedSeriesOfIdeal_mono {I J : LieIdeal R L} (h : I ≤ J) (k : ℕ) : D k I ≤ D k J :=
  derivedSeriesOfIdeal_le h (le_refl k)

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

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

Разделы

Аффилиация

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