mathlib3

73a61259 - 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`.