English
Saturated for a subgroup H is equivalent to the statement with g^n for integral powers, i.e., allowing negative exponents.
Русский
Насыщенность подгруппы H эквивалентна утверждению с целыми степенями, т.е. допускаются отрицательные экспоненты.
LaTeX
$$Saturated(H) ↔ ∀ (n : Z) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H$$
Lean4
@[to_additive]
theorem saturated_iff_zpow {H : Subgroup G} : Saturated H ↔ ∀ (n : ℤ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H :=
by
constructor
· intro hH n g hgn
cases n with
| ofNat n =>
simp only [Int.natCast_eq_zero, Int.ofNat_eq_coe, zpow_natCast] at hgn ⊢
exact hH hgn
| negSucc
n =>
suffices g ^ (n + 1) ∈ H by
refine (hH this).imp ?_ id
simp only [IsEmpty.forall_iff, Nat.succ_ne_zero]
simpa only [inv_mem_iff, zpow_negSucc] using hgn
· intro h n g hgn
specialize h n g
simp only [Int.natCast_eq_zero, zpow_natCast] at h
apply h hgn
