feat(linear_algebra/bilinear_form): generalize scalar instances, fix diamonds (#14358)
feat(linear_algebra/bilinear_form): generalize scalar instances, fix diamonds (#14358)

This fixes the zsmul and nsmul diamonds, makes sub definitionally better, and makes the scalar instance apply more generally.
This also adds `linear_map.comp_bilin_form`.

These changes bring the API more in line with `quadratic_form`.






leanprover-community/mathlib,leanprover-community/mathlib