feat(FreeGroup): characterize commutative/cyclic free groups

[vlad902]

Characterize cyclic/commutative free groups as being those on ≤ 1 generators. I generalize and move around some instances along the way to avoid new imports.

---

[github-actions]

PR summary 551b1cb5a7

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ instance (priority := 100) isCyclic_of_subsingleton [Subsingleton G] : IsCyclic G
+ instance [Subsingleton α] : IsCyclic (FreeGroup α) := by
+ instance _root_.FreeAddGroup.instIsAddCyclicOfSubsingleton [Subsingleton α] :
+ not_commute
+ not_isMulCommutative_of_nontrivial
+ subsingleton_iff_isCyclic
+ subsingleton_iff_isEmpty_or_unique
+ subsingleton_iff_isMulCommutative
- instance (priority := 100) isCyclic_of_subsingleton [Group α] [Subsingleton α] : IsCyclic α
- instance [Unique α] : IsAddCyclic (FreeAddGroup α)
- instance [Unique α] : IsCyclic (FreeGroup α)

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 551b1cb).

• +9 new declarations
• −2 removed declarations

+FreeAddGroup.instIsAddCyclicOfSubsingleton
+FreeAddGroup.not_addCommute
+FreeAddGroup.subsingleton_iff_isAddCommutative
+FreeAddGroup.subsingleton_iff_isAddCyclic
-FreeGroup.instIsAddCyclicFreeAddGroupOfUnique
+FreeGroup.instIsCyclicOfSubsingleton
-FreeGroup.instIsCyclicOfUnique
+FreeGroup.not_commute
+FreeGroup.subsingleton_iff_isCyclic
+FreeGroup.subsingleton_iff_isMulCommutative
+subsingleton_iff_isEmpty_or_unique

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 551b1cb5a7
Reference commit 3de5ed81cc

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[vlad902]

this instance is just moved to an earlier file

[vlad902]

This instance is just moved to an earlier file. I'd argue that since IsCyclic is defined in this file that it's reasonable to also state that the trivial group is cyclic here as well, but if Algebra.Group.Defs is too early, I could rename SpecificGroups.Cyclic.Basic to Cyclic.ZMod and then have SpecificGroups.Cyclic.Basic only import Algebra.Group.Basic with these two instances instead?