mathlib

3df3c617 - feat(linear_algebra/quadratic_form/basic): algebraic lemmas about `bilin_form.to_quadratic_form` (#16616)

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.