Commit 2022-09-30 13:10 3df3c617

feat(linear_algebra/quadratic_form/basic): algebraic lemmas about bilin_form.to_quadratic_form (#16616) Following the usual pattern, we defined the bundle additive morphism so that we can copy across the salient lemmas about sums. The polar_to_quadratic_form lemma in the diff was an existing lemma that has just been moved below the new semiring section.