Source: ProCGroups.FreeConstructions.Framework
1import ProCGroups.FreeProducts.UniversalProperty
3/-!
4# Finite generating data
6This file records concrete finite generating maps and finite families of
7subgroups. The companion bounds concatenate those maps to obtain explicit
8generating families for the ambient group.
9-/
11noncomputable section
13universe u
15namespace ProCGroups.FreeConstructions
17/-- The group is generated by at most \(r\) elements, expressed by an actual generating map. -/
18def AbstractGeneratorRankLE (G : Type u) [Group G] (r : Nat) : Prop :=
19 ∃ gen : Fin r → G, Subgroup.closure (Set.range gen) = ⊤
21end ProCGroups.FreeConstructions