Theorem IsSelfAdjoint.exists_nonneg_sub_nonneg

Modification history

2026-06-23 15:06
Mathlib/Algebra/Order/Star/Basic.lean
feat: introduce `SelfAdjointDecompose` class (#40530)
Added IsSelfAdjoint.exists_nonneg_sub_nonnegView on Github →