feat: add lemmas about doubly stochastic matrices

[dupuisf]

This PR adds a few basic lemmas about doubly stochastic matrices.

---

[github-actions]

PR summary 69fc0048aa

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ reindex_mem_doublyStochastic
+ reindex_mem_doublyStochastic_iff
+ sum_mulVec_of_mem_doublyStochastic
+ transpose_mem_doublyStochastic
+ transpose_mem_doublyStochastic_iff

You can run this locally as follows

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

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/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).

[j-loreaux]

@dupuisf can I instead interest you in taking over #28708 so we can get that over the line? Probably cleaning up some of the proofs there would be helpful.

[j-loreaux]

Doesn't this mean that grind will add a σ.permMatrix R ∈ doublyStochastic R n fact to the context whenever it sees σ : Equiv.Perm n? That seems a bit much to me, no?

[dupuisf]

No, here's the pattern this generates:

permMatrix_mem_doublyStochastic: [@Membership.mem _ (Submonoid _ _) _ (doublyStochastic #7 #6 #5 #4 #3 #2 #1) (@PEquiv.toMatrix _ _ _ _ _ _ (@Equiv.toPEquiv _ _ #0))]

So it's quite specific, it pretty much needs to see this exact statement.