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

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.

[x] depends on: #17454

Jul 21 '24 20:07 mans0954

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.