Theorem LinearMap.IsIdempotentElem.isPositive_iff_isSymmetric

Modification history

2025-07-27 22:47

Mathlib/Analysis/InnerProductSpace/Positive.lean

refactor(Analysis/InnerProductSpace/Positive): changing positivity on linear maps to use `IsSymmetric` instead of `IsSelfAdjoint` and finite-dimensionality (#27089) …

Added LinearMap.IsIdempotentElem.isPositive_iff_isSymmetric View on Github →