saturated_iff_npow — Mathlib

English

For a subgroup H, saturated is equivalent to: for all n ∈ N and g ∈ G, if g^n ∈ H, then n = 0 or g ∈ H.

Русский

Для подгруппы H насыщенность эквивалентна: для всех n ∈ N и g ∈ G, если g^n ∈ H, то n = 0 или g ∈ H.

LaTeX

$$Saturated(H) ↔ ∀ (n : ℕ) (g : G), g^n ∈ H → n = 0 ∨ g ∈ H$$

Lean4

@[to_additive]
theorem saturated_iff_npow {H : Subgroup G} : Saturated H ↔ ∀ (n : ℕ) (g : G), g ^ n ∈ H → n = 0 ∨ g ∈ H :=
  Iff.rfl

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