Commit 2024-07-13 17:36 98151c27

refactor(LinearAlgebra/QuadraticForm/Basic) : Generalise QuadraticForm to QuadraticMap (#7569) Most of the theory in LinearAlgebra/QuadraticForm/Basic also holds for Quadratic Maps with minimal modification. A quadratic form is just a special case of a quadratic map. To keep this PR to a reasonable size I have not attempted to generalise other files in LinearAlgebra/QuadraticForm - this can be done in subsequent PRs. To facilitate dot notation we also introduce LinearMap.BilinMap as an abbreviation for M →ₗ[R] M →ₗ[R] N. No attempt has been made to generalise all BilinForm results to BilinMap at this stage. Some results in LinearAlgebra/QuadraticForm/Basic are still stated for quadratic forms either because there was no obvious generalisation to quadratic maps, or the generalisation requires improvements elsewhere in Mathlib which can be considered in subsequent PRs. My motivation for introducing Quadratic Maps to Mathlib is that it would allow the definition of interesting non-associative structures such as quadratic Jordan Algebras and Jordan Pairs.