This generalizes as
```diff
-Matrix m m A ⊗[R] Matrix n n B ≃ₐ[R] Matrix (m × n) (m × n) (A ⊗[R] B)
+Matrix m m A ⊗[R] Matrix n n B ≃ₐ[S] Matrix (m × n) (m × n) (A ⊗[R] B)
```
where R / S / A is a tower of algebras. Notably, when `A` is commutative this allows `S := A`.

The module version is similarly generalized.

* master: (447 commits)
  chore(Data/Set): move very basic lemmas earlier (leanprover-community#25707)
  feat: preserve draft status when migrating PRs to fork (leanprover-community#25777)
  chore(Data/Set/Basic): deprecate lemmas that abuse the `Set α := α → Prop` defeq (leanprover-community#25669)
  refactor: redefine `ProperCone` as an `abbrev` for `ClosedSubmodule` (leanprover-community#25204)
  feat: interaction between ContinuousLinearMap.coprod and ContinuousLinearEquiv.prodComm (leanprover-community#25564)
  fix: outdated docstring (leanprover-community#25717)
  feat(MeasureTheory): convolution of measures with densities  (leanprover-community#25718)
  feat: make sure that the simp normal form of equiv-like classes pushes `symm` and `trans` to the right (leanprover-community#25604)
  feat(ModelTheory): Formula.iSup and iInf (leanprover-community#21948)
  feat(RingTheory/Polynomial/ContentIdeal): the content ideal of a polynomial. (leanprover-community#25333)
  fix: typo in labels_from_comment.yml (leanprover-community#25727)
  feat: is{Inducing,Embedding}_prodMkLeft (leanprover-community#25705)
  feat: check that the mathlib options exist (leanprover-community#25687)
  feat(Algebra/Group/Even): Add missing lemmas (leanprover-community#20818)
  refactor: make `Matrix.kroneckerTMulAlgEquiv` heterogeneous (leanprover-community#25693)
  feat: allow contributors to remove labels with comments (leanprover-community#25723)
  chore: disable build.yml and bors.yml on forks (leanprover-community#25722)
  feat: improvements to user_activity_report.py (leanprover-community#25721)
  chore: update the migration script to check for necessary permissions and prefer ssh if possible (leanprover-community#25701)
  chore: update the migration script to check for necessary permissions and prefer ssh if possible (leanprover-community#25701)
  ...

…er-community#25693)

This generalizes as
```diff
-Matrix m m A ⊗[R] Matrix n n B ≃ₐ[R] Matrix (m × n) (m × n) (A ⊗[R] B)
+Matrix m m A ⊗[R] Matrix n n B ≃ₐ[S] Matrix (m × n) (m × n) (A ⊗[R] B)
```
where R / S / A is a tower of algebras. Notably, when `A` is commutative this allows `S := A`.

The module version is similarly generalized.

…er-community#25693)

This generalizes as
```diff
-Matrix m m A ⊗[R] Matrix n n B ≃ₐ[R] Matrix (m × n) (m × n) (A ⊗[R] B)
+Matrix m m A ⊗[R] Matrix n n B ≃ₐ[S] Matrix (m × n) (m × n) (A ⊗[R] B)
```
where R / S / A is a tower of algebras. Notably, when `A` is commutative this allows `S := A`.

The module version is similarly generalized.

…er-community#25693)

This generalizes as
```diff
-Matrix m m A ⊗[R] Matrix n n B ≃ₐ[R] Matrix (m × n) (m × n) (A ⊗[R] B)
+Matrix m m A ⊗[R] Matrix n n B ≃ₐ[S] Matrix (m × n) (m × n) (A ⊗[R] B)
```
where R / S / A is a tower of algebras. Notably, when `A` is commutative this allows `S := A`.

The module version is similarly generalized.