rank_spec — Mathlib

English

Let G be a finitely generated group. There exists a finite subset S of G such that ⟨S⟩ = G and |S| = rank(G).

Русский

Пусть G — конечно порожденная группа. Существует конечное подмножество S ⊆ G такое, что ⟨S⟩ = G и |S| = rank(G).

LaTeX

$$$\exists S \in \mathrm{Finset}(G): S.\text{card} = \operatorname{rank}(G) \land \langle S \rangle = G.$$$

Lean4

@[to_additive]
theorem rank_spec [h : FG G] : ∃ S : Finset G, S.card = rank G ∧ .closure S = (⊤ : Subgroup G) :=
  @Nat.find_spec _ (Classical.decPred _) (fg_iff'.mp h)

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