feat(GroupTheory/IsPGroup): p-groups with coprime p are disjoint

[SnirBroshi]

Also their commutator is trivial.

Adds the same theorems to finite groups using Nat.card.

---

[github-actions]

PR summary 1eff6d210e

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ _root_.AddSubgroup.inf_eq_bot_of_coprime
+ commutator_eq_bot_of_coprime
+ commutator_eq_bot_of_coprime_natCard
+ commute_of_coprime
+ commute_of_coprime_natCard
+ disjoint_of_coprime
+ disjoint_of_coprime_natCard

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.

[tb65536]

What about just having commutator_eq_bot assuming Disjoint, and then plugging in disjoint_of_coprime_natCard later as needed (it just feels a bit overly specific to be composing them like this).

(We also have Subgroup.commute_of_normal_of_disjoint, but maybe that doesn't help streamline things any further here)

[tb65536]

This is just a special case of Subgroup.commute_of_normal_of_disjoint

[tb65536]

In general this feels like a fair amount of duplication for not much gain. Do you have an application in mind?

[SnirBroshi]

I agree the Commute versions are silly, I just didn't know we had Subgroup.commute_of_normal_of_disjoint (nor did I think about this generality so I didn't loogle it).
I like the ideas above, will do!