Theorem LinearMap.BilinForm.isPosSemidef_iff

Modification history

2025-10-08 04:09
Mathlib/LinearAlgebra/BilinearForm/Properties.lean
feat: define positive semidefinite sesquilinear maps (#28162) …
Added LinearMap.BilinForm.isPosSemidef_iffView on Github →