refactor(LinearAlgebra/BilinearForm/TensorProduct): Tensor products of bilinear maps

[mans0954]

Extend the results in Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean from Bilinear Forms to Bilinear Maps

Similarly for LinearAlgebra/QuadraticForm/TensorProduct.

I had originally intended to extend much more, but was blocked by not being able to extend LinearMap.IsSymm from forms to maps.

---

• depends on: [Merged by Bors] - feat: LinearEquiv.congrQuadraticMap and LinearEquiv.congrRight₂ #17454

[github-actions]

PR summary 21ea33a912

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.LinearAlgebra.BilinearForm.TensorProduct	1275	1277	+2 (+0.16%)
Mathlib.LinearAlgebra.QuadraticForm.TensorProduct	1308	1310	+2 (+0.15%)
Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange	1325	1327	+2 (+0.15%)

Import changes for all files

Files	Import difference
6 files Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Symmetric Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal Mathlib.LinearAlgebra.BilinearForm.TensorProduct Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange Mathlib.LinearAlgebra.QuadraticForm.TensorProduct Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries	2

---

Declarations diff

+ exists_quadraticMap_ne_zero
++ tensorDistrib
++ tensorDistrib_tmul
++- baseChange
++- baseChange_tmul
+-++ tmul

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.

[mans0954]

CC: @eric-wieser

[mans0954]

@eric-wieser did you have any further thoughts on this please?

[eric-wieser]

Can you fill out the "moves" section of the PR template to indicate that BilinMap.tmul and friends have moved to BilinForm.tmul?