Commit 2023-05-25 08:46 e7890e23

View on Github →

feat: port LinearAlgebra.Matrix.SesquilinearForm (#4315) Dot notation is broken here, but I don't think there is anything we can do about it.

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean

added theorem LinearMap.SeparatingLeft.toMatrix₂'

added theorem LinearMap.SeparatingLeft.toMatrix₂

added theorem LinearMap.mul_toMatrix'

added theorem LinearMap.mul_toMatrix₂'_mul

added theorem LinearMap.mul_toMatrix₂

added theorem LinearMap.mul_toMatrix₂_mul

added theorem LinearMap.nondegenerate_toMatrix_iff

added theorem LinearMap.nondegenerate_toMatrix₂'_iff

added theorem LinearMap.separatingLeft_iff_det_ne_zero

added theorem LinearMap.separatingLeft_of_det_ne_zero

added theorem LinearMap.separatingLeft_toLinearMap₂'_iff_det_ne_zero

added theorem LinearMap.separatingLeft_toLinearMap₂'_of_det_ne_zero'

added theorem LinearMap.toLinearMap₂'Aux_toMatrix₂Aux

added theorem LinearMap.toMatrix'_toLinearMap₂'

added theorem LinearMap.toMatrix'_toLinearMapₛₗ₂'

added def LinearMap.toMatrix₂'

added theorem LinearMap.toMatrix₂'_apply

added theorem LinearMap.toMatrix₂'_comp

added theorem LinearMap.toMatrix₂'_compl₁₂

added theorem LinearMap.toMatrix₂'_compl₂

added theorem LinearMap.toMatrix₂'_mul

added def LinearMap.toMatrix₂Aux

added theorem LinearMap.toMatrix₂Aux_apply

added theorem LinearMap.toMatrix₂Aux_eq

added theorem LinearMap.toMatrix₂_apply

added theorem LinearMap.toMatrix₂_basisFun

added theorem LinearMap.toMatrix₂_comp

added theorem LinearMap.toMatrix₂_compl₁₂

added theorem LinearMap.toMatrix₂_compl₂

added theorem LinearMap.toMatrix₂_mul

added theorem LinearMap.toMatrix₂_mul_basis_toMatrix

added theorem LinearMap.toMatrix₂_symm

added theorem LinearMap.toMatrix₂_toLinearMap₂

added def LinearMap.toMatrixₛₗ₂'

added theorem LinearMap.toMatrixₛₗ₂'_apply

added theorem LinearMap.toMatrixₛₗ₂'_symm

added def Matrix.IsAdjointPair

added def Matrix.IsSelfAdjoint

added def Matrix.IsSkewAdjoint

added theorem Matrix.Nondegenerate.toLinearMap₂'

added theorem Matrix.Nondegenerate.toLinearMap₂

added theorem Matrix.isAdjointPair_equiv

added theorem Matrix.separatingLeft_toLinearMap₂'_iff

added theorem Matrix.separatingLeft_toLinearMap₂'_iff_separatingLeft_toLinearMap₂

added theorem Matrix.separatingLeft_toLinearMap₂_iff

added def Matrix.toLinearMap₂'

added def Matrix.toLinearMap₂'Aux

added theorem Matrix.toLinearMap₂'Aux_stdBasis

added theorem Matrix.toLinearMap₂'_apply'

added theorem Matrix.toLinearMap₂'_apply

added theorem Matrix.toLinearMap₂'_comp

added theorem Matrix.toLinearMap₂'_stdBasis

added theorem Matrix.toLinearMap₂'_toMatrix'

added theorem Matrix.toLinearMap₂_apply

added theorem Matrix.toLinearMap₂_basisFun

added theorem Matrix.toLinearMap₂_compl₁₂

added theorem Matrix.toLinearMap₂_symm

added theorem Matrix.toLinearMap₂_toMatrix₂

added def Matrix.toLinearMapₛₗ₂'

added theorem Matrix.toLinearMapₛₗ₂'_apply

added theorem Matrix.toLinearMapₛₗ₂'_aux_eq

added theorem Matrix.toLinearMapₛₗ₂'_stdBasis

added theorem Matrix.toLinearMapₛₗ₂'_symm

added theorem Matrix.toLinearMapₛₗ₂'_toMatrix'

added theorem Matrix.toMatrix₂Aux_toLinearMap₂'Aux

added theorem isAdjointPair_toLinearMap₂'

added theorem isAdjointPair_toLinearMap₂

added theorem mem_pairSelfAdjointMatricesSubmodule

added theorem mem_selfAdjointMatricesSubmodule

added theorem mem_skewAdjointMatricesSubmodule

added def pairSelfAdjointMatricesSubmodule

added def selfAdjointMatricesSubmodule

added def skewAdjointMatricesSubmodule