FG — Mathlib · SciLib

English

A subgroup P of G is finitely generated if and only if there exists a finite subset S of G such that the closure of S equals P.

Русский

Подгруппа P группы G конечнопорождается тогда и только тогда, когда существует конечное подмножество S ⊆ G такое, что замыкание S равно P.

LaTeX

$$$\text{FG}(P) \iff \exists S : Finset G, Subgroup.closure (S.ToSet) = P$$$

Lean4

/-- A subgroup of `G` is finitely generated if it is the closure of a finite subset of `G`. -/
@[to_additive]
def FG (P : Subgroup G) : Prop :=
  ∃ S : Finset G, Subgroup.closure ↑S = P

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