mathlib3

abf2ab4d - feat(linear_algebra/quadratic_form): associated bilinear form over noncommutative rings (#6585)

feat(linear_algebra/quadratic_form): associated bilinear form over noncommutative rings (#6585) The `associated` bilinear form to a quadratic form is currently constructed for commutative rings, but nearly the same construction works without a commutativity hypothesis (the only part that fails is that the operation of performing the construction is now an `add_monoid_hom` rather than a `linear_map`. I provide this construction, naming it `associated'`. Needed for #5814 (not exactly a dependency since we can merge a non-optimal version of that PR before this one is merged). Co-authored-by: Eric Wieser <wieser.eric@gmail.com>