derivedSeries_baseChange — Mathlib

English

For any I in a Lie algebra L and any A with algebra structure over R, the k-th derived series respects base change: derivedSeriesBaseChange k I = baseChange_k (derivedSeries k I).

Русский

Для идеала I в L и любой базы A над R выполняется сохранение производного ряда при базовом переносе: derivedSeriesBaseChange k I = baseChange_k (derivedSeries k I).

LaTeX

$$$\text{derivedSeries}_A(k, I.baseChange A) = (\text{derivedSeries}_R(l, k, I)).baseChange A$$$

Lean4

@[simp]
theorem derivedSeries_baseChange {A : Type*} [CommRing A] [Algebra R A] (k : ℕ) :
    derivedSeries A (A ⊗[R] L) k = (derivedSeries R L k).baseChange A := by
  rw [derivedSeries_def, derivedSeries_def, ← derivedSeriesOfIdeal_baseChange, LieSubmodule.baseChange_top]

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