Commit 2026-01-19 11:57 7f8939ff

View on Github →

chore(LinearAlgebra/Matrix/BilinearForm): sort out namespaces (#34057) About 90% of the defs and theorems about bilinear forms are in the LinearMap.BilinForm namespace, but there are a dozen or so which are in BilinForm or BilinearForm. This PR imposes a consistent naming scheme. This is a preliminary to refactoring LinearAlgebra.BilinForm.Nondegenerate as discussed in this zulip thread.

Estimated changes

deleted theorem BilinForm.mul_toMatrix
deleted theorem BilinForm.toMatrix_apply
deleted theorem BilinForm.toMatrix_comp
deleted theorem BilinForm.toMatrix_mul
deleted theorem BilinForm.toMatrix_symm
modified theorem Matrix.toBilin_symm
deleted theorem toBilin'Aux_toMatrixAux