Commit 2024-10-15 09:59 5f0628ea

View on Github →

chore: remove and rename variables (#17760) I also relabeled some indices, since some intermediate variables vanished in the process.

Estimated changes

modified theorem BilinForm.mul_toMatrix
modified theorem BilinForm.mul_toMatrix_mul
modified def BilinForm.toMatrixAux
modified theorem BilinForm.toMatrix_apply
modified theorem BilinForm.toMatrix_comp
modified theorem BilinForm.toMatrix_compLeft
modified theorem BilinForm.toMatrix_mul
modified theorem BilinForm.toMatrix_toBilin
modified theorem BilinearForm.toMatrixAux_eq
modified theorem Matrix.isAdjointPair_equiv'
modified def Matrix.toBilin'
modified def Matrix.toBilin'Aux
modified theorem Matrix.toBilin'Aux_eq
modified theorem Matrix.toBilin'Aux_single
modified theorem Matrix.toBilin'_apply'
modified theorem Matrix.toBilin'_apply
modified theorem Matrix.toBilin'_comp
modified theorem Matrix.toBilin'_single
modified theorem Matrix.toBilin'_stdBasis
modified theorem Matrix.toBilin'_toMatrix'
modified theorem Matrix.toBilin_apply
modified theorem Matrix.toBilin_basisFun
modified theorem Matrix.toBilin_comp
modified theorem Matrix.toBilin_toMatrix
modified theorem toBilin'Aux_toMatrixAux