feat(linear_algebra/bilinear_form, linear_algebra/quadratic_form): bilinear, quadratic forms on finsupp

[hrmacbeth]

A "matrix" of bilinear forms on M on a type α (possibly infinite) induces a bilinear form on α →₀ M, and thence (via bilin_form.to_quadratic_form a quadratic form. In particular, define the "Euclidean" (sum-of-squares) quadratic form on α →₀ M.

Zulip

---

• [x] depends on: #6565
• [x] depends on: #6824

[bors[bot]]

:v: hrmacbeth can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[tb65536]

@hrmacbeth Do you have plans to return to this at some point?

[jcommelin]

@hrmacbeth :ping_pong:

[github-actions[bot]]

This PR/issue depends on:

• ~~leanprover-community/mathlib#6565~~
• ~~leanprover-community/mathlib#6824~~ By Dependent Issues (🤖). Happy coding!