lowerCentralSeries_isDescendingCentralSeries

English

The lower central series is a descending central series.

Русский

Нижняя центральная серия является падающей центральной серией.

LaTeX

$$$IsDescendingCentralSeries(\\lowerCentralSeries G)$$$

Lean4

/-- The lower central series of a group is a descending central series. -/
theorem lowerCentralSeries_isDescendingCentralSeries : IsDescendingCentralSeries (lowerCentralSeries G) :=
  by
  constructor
  · rfl
  intro x n hxn g
  exact commutator_mem_commutator hxn (mem_top g)

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