derivedSeries_add_eq_bot — Mathlib

English

If the k-th derived series of I and the l-th derived series of J are both zero, then the (k+l)-th derived series of I+J is zero: derivedSeries R (I+J) (k+l) = ⊥.

Русский

Если D_k I = ⊥ и D_l J = ⊥, то D_(k+l) (I+J) = ⊥.

LaTeX

$$$D(k+l)(I+J) = \bot$$$

Lean4

theorem derivedSeries_add_eq_bot {k l : ℕ} {I J : LieIdeal R L} (hI : derivedSeries R I k = ⊥)
    (hJ : derivedSeries R J l = ⊥) : derivedSeries R (I + J) (k + l) = ⊥ :=
  by
  rw [LieIdeal.derivedSeries_eq_bot_iff] at hI hJ ⊢
  rw [← le_bot_iff]
  let D := derivedSeriesOfIdeal R L; change D k I = ⊥ at hI; change D l J = ⊥ at hJ
  calc
    D (k + l) (I + J) ≤ D k I + D l J := derivedSeriesOfIdeal_add_le_add I J k l
    _ ≤ ⊥ := by rw [hI, hJ]; simp

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