upperCentralSeries_one — Mathlib

English

The first nontrivial term of the upper central series is the center of G.

Русский

Первый ненулевой член верхней центральной серии равен центру группы.

LaTeX

$$$\mathrm{upperCentralSeries}(G,1)=Z(G)$$$

Lean4

@[simp]
theorem upperCentralSeries_one : upperCentralSeries G 1 = center G :=
  by
  ext
  simp only [upperCentralSeries, upperCentralSeriesAux, upperCentralSeriesStep, mem_bot, mem_mk, Submonoid.mem_mk,
    Subsemigroup.mem_mk, Set.mem_setOf_eq, mem_center_iff]
  exact forall_congr' fun y => by rw [mul_inv_eq_one, mul_inv_eq_iff_eq_mul, eq_comm]

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