mathlib

be1af7ce - feat(linear_algebra/quadratic_form): provide `distrib_mul_action S (quadratic_form M R)` when `S` has no addition. (#7443)

feat(linear_algebra/quadratic_form): provide `distrib_mul_action S (quadratic_form M R)` when `S` has no addition. (#7443) The end goal here is to provide `has_scalar (units R) (quadratic_form M R)` for possible use in #7427