refactor(GroupTheory/Torsion): make primaryComponent total

[rosborn]

Change primaryComponent to the IsPGroup-style {g | ∃ k, g ^ p ^ k = 1}, making the definitions total over p : ℕ without requiring [Fact p.Prime].

---

Needed to use primaryComponent under a binder where it can't synthesize [Fact p.Prime] (e.g., ⨆ p : (Nat.card G).primeFactors, primaryComponent G p.val and similar family-shaped iSup / Finset.prod patterns). The new carrier agrees with the previous {g | ∃ n, orderOf g = p^n} on primes, so existing [Fact p.Prime] API is unaffected.

Discussed on Zulip

[github-actions]

PR summary 197b6725be

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

++ mem_primaryComponent
++ mem_primaryComponent_iff_orderOf

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.

---

No changes to strong technical debt.

No changes to weak technical debt.