feat(LinearAlgebra/QuadraticForm): radical of a quadratic form

[loefflerd]

Define the radical of a quadratic form, and show that its dimension is invariant under equivalences.

---

This is a step on the way to Sylvester's law of inertia (#34204).

• depends on: [Merged by Bors] - feat(LinearAlgebra/BilinearForm): Harmonize definitions of "Nondegenerate" #34110

[github-actions]

PR summary cf6b5548c3

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.LinearAlgebra.QuadraticForm.Radical (new file)	1548

---

Declarations diff

+ Equivalent.rank_radical_eq
+ IsometryEquiv.map_radical
+ LinearIndependent.linearIndepOn_univ
+ Nondegenerate
+ Pi.dim_spanSubset
+ apply_symm_apply
+ coe_symm_toLinearEquiv
+ finrank_radical_of_equiv_weightedSumSquares
+ le_radical_iff
+ lift
+ lift_aux
+ lift_mk
+ linearIndepOn
+ linearIndepOn_univ_iff
+ mem_radical_iff'
+ mem_spanSubset_iff
+ nondegenerate_associated_iff
+ nondegenerate_iff_radical_eq_bot
+ nondegenerate_polar_iff
+ radical
+ radical_eq_ker_associated
+ radical_eq_ker_polarBilin
+ radical_le_ker_polarBilin
+ radical_weightedSumSquares
+ spanSubset
+ symm_apply_apply
- linearIndepOn_univ

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(LinearAlgebra/BilinearForm): Harmonize definitions of "Nondegenerate" #34110
  By Dependent Issues (🤖). Happy coding!

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.