Commit 2025-10-08 04:09 64ce1d71

View on Github →

feat: define positive semidefinite sesquilinear maps (#28162) Following what is done for IsSymm, we duplicate the definition for bilinear forms.

Estimated changes

Modified Mathlib/LinearAlgebra/BilinearForm/Properties.lean

added structure LinearMap.BilinForm.IsNonneg

added structure LinearMap.BilinForm.IsPosSemidef

added theorem LinearMap.BilinForm.isNonneg_def

added theorem LinearMap.BilinForm.isNonneg_iff

added theorem LinearMap.BilinForm.isNonneg_zero

added theorem LinearMap.BilinForm.isPosSemidef_def

added theorem LinearMap.BilinForm.isPosSemidef_iff

added theorem LinearMap.BilinForm.isPosSemidef_zero

Modified Mathlib/LinearAlgebra/SesquilinearForm.lean

added structure LinearMap.IsNonneg

added structure LinearMap.IsPosSemidef

added theorem LinearMap.isNonneg_def

added theorem LinearMap.isNonneg_zero

added theorem LinearMap.isPosSemidef_def

added theorem LinearMap.isPosSemidef_zero