English
If G ≃* H is a group isomorphism, then IsNilpotent G ⇄ IsNilpotent H.
Русский
Если существуют изоморфизмы групп G и H, то нильпотентность сохраняется: IsNilpotent G ⇄ IsNilpotent H.
LaTeX
$$$\text{IsNilpotent}(G) \iff \text{IsNilpotent}(H)$ for any isomorphism $e:G\simeq H$.$$
Lean4
theorem is_descending_rev_series_of_is_ascending {H : ℕ → Subgroup G} {n : ℕ} (hn : H n = ⊤)
(hasc : IsAscendingCentralSeries H) : IsDescendingCentralSeries fun m : ℕ => H (n - m) :=
by
obtain ⟨h0, hH⟩ := hasc
refine ⟨hn, fun x m hx g => ?_⟩
dsimp at hx
by_cases hm : n ≤ m
· rw [tsub_eq_zero_of_le hm, h0, Subgroup.mem_bot] at hx
subst hx
rw [show (1 : G) * g * (1⁻¹ : G) * g⁻¹ = 1 by group]
exact Subgroup.one_mem _
· push_neg at hm
apply hH
convert hx using 1
rw [tsub_add_eq_add_tsub (Nat.succ_le_of_lt hm), Nat.succ_eq_add_one, Nat.add_sub_add_right]
