is_ascending_rev_series_of_is_descending

English

IsNilpotent (⊤ : Subgroup G) ⇔ IsNilpotent G.

Русский

IsNilpotent (⊤ как подгруппа G) ⇔ IsNilpotent G.

LaTeX

$$$\text{IsNilpotent}((\top:\mathrm{Subgroup}(G))) \iff \text{IsNilpotent}(G)$$$

Lean4

theorem is_ascending_rev_series_of_is_descending {H : ℕ → Subgroup G} {n : ℕ} (hn : H n = ⊥)
    (hdesc : IsDescendingCentralSeries H) : IsAscendingCentralSeries fun m : ℕ => H (n - m) :=
  by
  obtain ⟨h0, hH⟩ := hdesc
  refine ⟨hn, fun x m hx g => ?_⟩
  dsimp only at hx ⊢
  by_cases hm : n ≤ m
  · have hnm : n - m = 0 := tsub_eq_zero_iff_le.mpr hm
    rw [hnm, h0]
    exact mem_top _
  · push_neg at hm
    convert hH x _ hx g using 1
    rw [tsub_add_eq_add_tsub (Nat.succ_le_of_lt hm), Nat.succ_eq_add_one, Nat.add_sub_add_right]

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