mathlib

ef69547c - feat(group_theory/finiteness): Define the minimum number of generators (#12765)

feat(group_theory/finiteness): Define the minimum number of generators (#12765) The PR adds a definition of the minimum number of generators, which will be needed for a statement of Schreier's lemma.