…p.IsSymm.tmul`

lemma. We should have this lemma for both quadratic forms and quadratic maps
since the tensor product of two quadratic forms, regarded as maps is not
definitionally the same as their tensor product as forms (the former takes
values in `R ⊗ R`, the latter in `R`).

As a result of this, I was able to undo some of the changes to fix existing
proofs which were otherwise needed adjustment. Also, I have undone the change to
`LinearMap.BilinForm.baseChange`. The proposed new definition was actually
defeq but less useful (and anyway was only changed to help close a proof which
no longer needs this change).

I have also made a set of minor style tweaks: removing redundant argument naming,
enforcing "left of colon", avoiding line breaks inside terms.

Finally for lemmas whose statements actually include a term of type `LinearMap.IsSymm`,
I have duplicated rather than adjusting them: otherwise we are breaking the naming
contract. This means a small amount of duplication is necessary but I think this is
preferable: unless / until we develop very thorough and much more consistent API to
unify bilinear forms and maps, we should optimise these statements for the more
common case (forms).