derivedSeries_eq_derivedSeriesOfIdeal_map

English

The derived series commutes with the map I.incl up to equality: (derivedSeries R I k).map I.incl = derivedSeriesOfIdeal R L k I.

Русский

Производный ряд коммутирует отображение I.incl: (derivedSeries R I k).map I.incl = derivedSeriesOfIdeal R L k I.

LaTeX

$$$(\text{derivedSeries} \ R \ I \ k).map I.incl = \text{derivedSeriesOfIdeal} R L k I$$$

Lean4

theorem derivedSeries_eq_derivedSeriesOfIdeal_map (k : ℕ) :
    (derivedSeries R I k).map I.incl = derivedSeriesOfIdeal R L k I :=
  by
  rw [derivedSeries_eq_derivedSeriesOfIdeal_comap, map_comap_incl, inf_eq_right]
  apply derivedSeriesOfIdeal_le_self

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