Commit 2026-10-10 10:24 8f74e84f
View on Github →refactor(SpecificGroups/Cyclic/Basic): split out heavy-import file (#44473)
Basic.lean includes basic properties of cyclic groups as well as heavy-import properties of about finite cyclic groups/subgroups of cyclic groups. Split out the heavier import theorems into Cyclic/Subgroup.lean, and keep the basic properties in Basic.lean. This is a response to PR review for #41988.