refactor(Algebra/Bilinear): generalize to non-commutative base rings

[eric-wieser]

This removes unnecessary IsScalarTower R A A and SMulCommClass R A A arguments from LinearMap.mulLeft and LinearMap.mulRight, respectively.

As described in the new docstring, this allows respective specializations to R := Aᵐᵒᵖ and R := A.

Unfortunately all of the lemmas have to be reordered to take advantage of these relaxed assumptions.

In the chaos, a few lemmas also became generalized to non-unital rings.

There is some overlap here with DistribMulAction.toLinearMap, but that doesn't work in the case of non-unital rings.

---

[github-actions]

PR summary 06fbed383e

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

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

[eric-wieser]

!bench

[leanprover-bot]

Here are the benchmark results for commit 06fbed3.
There were significant changes against commit 4362117:

  Benchmark                             Metric         Change
  ===========================================================
- ~Mathlib.RingTheory.PiTensorProduct   instructions    13.9%

[github-actions]

File	Instructions	%
build	+24.652⬝10⁹	(+0.01%)
Mathlib.RingTheory.PiTensorProduct	+11.307⬝10⁹	(+13.85%)
Mathlib.RingTheory.TensorProduct.Basic	+9.94⬝10⁹	(+2.84%)
Mathlib.LinearAlgebra.TensorProduct.Graded.Internal	+3.145⬝10⁹	(+1.22%)
Mathlib.Algebra.Algebra.Bilinear	+2.906⬝10⁹	(+16.49%)

2 files, Instructions -2.0⬝10⁹

File	Instructions	%
Mathlib.LinearAlgebra.CliffordAlgebra.Even	-1.319⬝10⁹	(-1.26%)
Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv	-1.351⬝10⁹	(-1.02%)