Commit 2025-07-26 21:20 bc035eec

View on Github →

feat: api for symmetric bilinear forms (#26274) Change the definition of BilinForm.IsSymm to make it a structure, in order to extend it to define ContinuousBilinForm.IsPosSemidef in #26315. Prove polarization identity. Prove two lemmas about BilinForm.toMatrix.

Estimated changes

Modified Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean

Modified Mathlib/LinearAlgebra/BilinearForm/Properties.lean

modified theorem LinearMap.BilinForm.IsSymm.isRefl

added theorem LinearMap.BilinForm.IsSymm.polarization

added structure LinearMap.BilinForm.IsSymm

deleted def LinearMap.BilinForm.IsSymm

added theorem LinearMap.BilinForm.ext_iff_of_isSymm

added theorem LinearMap.BilinForm.ext_of_isSymm

added theorem LinearMap.BilinForm.isSymm_def

added theorem LinearMap.BilinForm.isSymm_iff

added theorem LinearMap.BilinForm.isSymm_iff_basis

modified theorem LinearMap.BilinForm.isSymm_iff_flip

modified theorem LinearMap.BilinForm.isSymm_zero

Modified Mathlib/LinearAlgebra/Matrix/BilinearForm.lean

added theorem BilinForm.apply_eq_dotProduct_toMatrix_mulVec

added theorem BilinForm.dotProduct_toMatrix_mulVec

Modified Mathlib/RingTheory/Trace/Defs.lean

modified theorem Algebra.traceForm_isSymm