Commit 2025-10-24 10:20 301d9925
View on Github →chore(GroupTheory/Index): move awkwardly placed lemmas (#30832)
The lemmas Subgroup.toSubmonoid_zpowers and Submonoid.powers_le_zpowers were awkwardly placed at the top of Index.lean despite being unrelated to the contents of that file. I have moved them to directly afterward closure_toSubmonoid which is thematically similar and also the key ingredient in the proof.