Commit 2024-07-01 13:36 2d9a1772

chore: move two lemmas about the exponent and the rank of groups (#14181) These are strictly speaking not specific to Schreier's lemma, but are only used there and bring in somewhat heavy imports. This change flips the longest pole in mathlib back to topology/analysis.