Commit 2021-03-15 09:03 abf2ab4d

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).