Commit 2024-02-01 12:43 fe642cfe

View on Github →

refactor(LinearAlgebra/QuadraticForm/Basic): Use bilinear maps for the companion (#10097) This PR replaces the companion (B : BilinForm R M) of a quadratic form with a bilinear map (B : M →ₗ[R] M →ₗ[R] R). This is intended as a baby step towards generalising quadratic forms to quadratic maps. In the future we could allow for companion bilinear or even sesquilinear maps into an R-module.

Estimated changes

Modified Mathlib/LinearAlgebra/BilinearMap.lean

added def LinearMap.linMulLin

Modified Mathlib/LinearAlgebra/QuadraticForm/Basic.lean

modified def BilinForm.toQuadraticForm

modified def BilinForm.toQuadraticFormLinearMap

modified theorem BilinForm.toQuadraticForm_smul

added def LinearMap.toQuadraticForm

modified theorem QuadraticForm.choose_exists_companion

modified theorem QuadraticForm.exists_companion

added def QuadraticForm.polarLinearMap₂

modified def QuadraticForm.weightedSumSquares

Modified Mathlib/LinearAlgebra/QuadraticForm/Dual.lean

deleted theorem BilinForm.dualProd.toQuadraticForm

deleted def BilinForm.dualProd

deleted theorem BilinForm.isSymm_dualProd

deleted theorem BilinForm.nondenerate_dualProd

added theorem LinearMap.dualProd.toQuadraticForm

added def LinearMap.dualProd

added theorem LinearMap.isSymm_dualProd

added theorem LinearMap.separatingLeft_dualProd