Commit 2023-05-26 20:04 a1d2ab60

View on Github →

feat: port LinearAlgebra.Matrix.BilinearForm (#4361)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Matrix/BilinearForm.lean

added theorem BilinForm.Nondegenerate.toMatrix'

added theorem BilinForm.Nondegenerate.toMatrix

added theorem BilinForm.mul_toMatrix'

added theorem BilinForm.mul_toMatrix'_mul

added theorem BilinForm.mul_toMatrix

added theorem BilinForm.mul_toMatrix_mul

added theorem BilinForm.nondegenerate_iff_det_ne_zero

added theorem BilinForm.nondegenerate_of_det_ne_zero

added theorem BilinForm.nondegenerate_toBilin'_iff_det_ne_zero

added theorem BilinForm.nondegenerate_toBilin'_of_det_ne_zero'

added theorem BilinForm.nondegenerate_toMatrix'_iff

added theorem BilinForm.nondegenerate_toMatrix_iff

added def BilinForm.toMatrix'

added theorem BilinForm.toMatrix'_apply

added theorem BilinForm.toMatrix'_comp

added theorem BilinForm.toMatrix'_compLeft

added theorem BilinForm.toMatrix'_compRight

added theorem BilinForm.toMatrix'_mul

added theorem BilinForm.toMatrix'_symm

added theorem BilinForm.toMatrix'_toBilin'

added def BilinForm.toMatrixAux

added theorem BilinForm.toMatrixAux_apply

added theorem BilinForm.toMatrixAux_stdBasis

added theorem BilinForm.toMatrix_apply

added theorem BilinForm.toMatrix_basisFun

added theorem BilinForm.toMatrix_comp

added theorem BilinForm.toMatrix_compLeft

added theorem BilinForm.toMatrix_compRight

added theorem BilinForm.toMatrix_mul

added theorem BilinForm.toMatrix_mul_basis_toMatrix

added theorem BilinForm.toMatrix_symm

added theorem BilinForm.toMatrix_toBilin

added theorem BilinearForm.toMatrixAux_eq

added theorem Matrix.Nondegenerate.toBilin'

added theorem Matrix.Nondegenerate.toBilin

added theorem Matrix.isAdjointPair_equiv'

added theorem Matrix.nondegenerate_toBilin'_iff

added theorem Matrix.nondegenerate_toBilin'_iff_nondegenerate_toBilin

added theorem Matrix.nondegenerate_toBilin_iff

added def Matrix.toBilin'

added def Matrix.toBilin'Aux

added theorem Matrix.toBilin'Aux_eq

added theorem Matrix.toBilin'Aux_stdBasis

added theorem Matrix.toBilin'_apply'

added theorem Matrix.toBilin'_apply

added theorem Matrix.toBilin'_comp

added theorem Matrix.toBilin'_stdBasis

added theorem Matrix.toBilin'_symm

added theorem Matrix.toBilin'_toMatrix'

added theorem Matrix.toBilin_apply

added theorem Matrix.toBilin_basisFun

added theorem Matrix.toBilin_comp

added theorem Matrix.toBilin_symm

added theorem Matrix.toBilin_toMatrix

added theorem isAdjointPair_toBilin'

added theorem isAdjointPair_toBilin

added theorem mem_pairSelfAdjointMatricesSubmodule'

added theorem mem_selfAdjointMatricesSubmodule'

added theorem mem_skewAdjointMatricesSubmodule'

added def pairSelfAdjointMatricesSubmodule'

added def selfAdjointMatricesSubmodule'

added def skewAdjointMatricesSubmodule'

added theorem toBilin'Aux_toMatrixAux