derivedSeries_succ_eq_top_iff — Mathlib

English

For any n, the (n+1)-st derived series of L equals the top if and only if the first derived series of L equals the top.

Русский

Для любого натурального n равно, что (n+1)-я производящая серия Ли-алгебры равна верхнему пределу, если и только если первая производящая серия равна верхнему пределу.

LaTeX

$$$\mathrm{derivedSeries}_{R} L (n+1) = \top \;\iff\; \mathrm{derivedSeries}_{R} L 1 = \top$$$

Lean4

theorem derivedSeries_succ_eq_top_iff (n : ℕ) : derivedSeries R L (n + 1) = ⊤ ↔ derivedSeries R L 1 = ⊤ :=
  by
  simp only [derivedSeries_def]
  induction n with
  | zero => simp
  | succ n ih =>
    rw [derivedSeriesOfIdeal_succ]
    refine ⟨fun h ↦ ?_, fun h ↦ by rwa [ih.mpr h]⟩
    rw [← ih, eq_top_iff]
    conv_lhs => rw [← h]
    exact LieSubmodule.lie_le_right _ _

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