Commit 2023-09-06 16:43 7878119e

View on Github →

feat: port LinearAlgebra.QuadraticForm.Dual (#6885)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/QuadraticForm/Dual.lean

added theorem BilinForm.dualProd.toQuadraticForm

added def BilinForm.dualProd

added theorem BilinForm.isSymm_dualProd

added theorem BilinForm.nondenerate_dualProd

added def QuadraticForm.dualProd

added def QuadraticForm.dualProdIsometry

added def QuadraticForm.dualProdProdIsometry

added def QuadraticForm.toDualProd

added theorem QuadraticForm.toDualProd_isometry