derivedLength_eq_derivedLengthOfIdeal

English

The derived length of a Lie ideal I equals the derived length of I viewed inside L, i.e., they are the same numerical value.

Русский

Длина производной идеала I равна длине производной, вычисляемой внутри L; значения совпадают.

LaTeX

$$$\mathrm{derivedLength}(R,I) = \mathrm{derivedLengthOfIdeal}(R,L,I).$$$

Lean4

theorem derivedLength_eq_derivedLengthOfIdeal (I : LieIdeal R L) : derivedLength R I = derivedLengthOfIdeal R L I :=
  by
  let s₁ := {k | derivedSeries R I k = ⊥}
  let s₂ := {k | derivedSeriesOfIdeal R L k I = ⊥}
  change sInf s₁ = sInf s₂
  congr; ext k; exact I.derivedSeries_eq_bot_iff k

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