Saturated — Mathlib

English

A subgroup H of G is saturated if whenever g^n ∈ H for n ∈ N, then either n = 0 or g ∈ H.

Русский

Подгруппа H группы G называется насыщенной, если для каждого n ∈ N и g ∈ G, если g^n ∈ H, то либо n = 0, либо g ∈ H.

LaTeX

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

Lean4

/-- A subgroup `H` of `G` is *saturated* if for all `n : ℕ` and `g : G` with `g^n ∈ H`
we have `n = 0` or `g ∈ H`. -/
@[to_additive /-- An additive subgroup `H` of `G` is *saturated* if for all `n : ℕ` and `g : G` with `n•g ∈ H` we
    have `n = 0` or `g ∈ H`. -/
    ]
def Saturated (H : Subgroup G) : Prop :=
  ∀ ⦃n g⦄, g ^ n ∈ H → n = 0 ∨ g ∈ H

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