Commit 2024-11-15 23:56 22b57433

View on Github →

feat(Algebra.Order.Star.Basic): add aesop lemma IsSelfAdjoint.mul_self_nonneg. (#19033) Includes the simple fact that in a StarOrderedRing, selfadjoint elements have nonnegative squares.

Estimated changes