English
Let G be a finitely generated group. The rank of G is the smallest possible size of a generating subset of G. Equivalently, rank(G) = min{ |S| : S ⊆ G and ⟨S⟩ = G }.
Русский
Пусть G является конечно порожденной группой. Ранг G есть наименьшая возможная мощность порождающего подмножества G. Эквивалентно: rank(G) = min{ |S| : S ⊆ G и ⟨S⟩ = G }.
LaTeX
$$$\operatorname{rank}(G) = \min\{ |S| : S \subseteq G, \langle S \rangle = G \} \quad (\text{при } FG\ G). $$$
Lean4
/-- The minimum number of generators of a group. -/
@[to_additive /-- The minimum number of generators of an additive group. -/
]
noncomputable def rank [h : FG G] : ℕ :=
@Nat.find _ (Classical.decPred _) (fg_iff'.mp h)
