2025-07-27 22:47
Mathlib/Analysis/InnerProductSpace/Symmetric.lean
refactor(Analysis/InnerProductSpace/Positive): changing positivity on linear maps to use `IsSymmetric` instead of `IsSelfAdjoint` and finite-dimensionality (#27089) …
Added LinearMap.IsSymmetric.intCast