derivedSeries_def

Mathlib.Algebra.Lie.Solvable

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

English

The derived series is the same as the k-th derived of the top ideal: derivedSeries R L k = D_k ⊤.

Русский

Производный ряд совпадает с k-м производным над верхним идеалом: derivedSeries_R L k = D_k ⊤.

LaTeX

$$$\text{derivedSeries}(k) = D(k) \top$$$

Lean4

theorem derivedSeries_def (k : ℕ) : derivedSeries R L k = derivedSeriesOfIdeal R L k ⊤ :=
  rfl

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

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

Разделы

Аффилиация

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