Theorem IsSelfAdjoint.exp_nonneg

Modification history

2024-09-02 17:15
Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean
feat(ContinuousFunctionalCalculus): add lemmas for automation and simp/aesop tags (#16050) …
Added IsSelfAdjoint.exp_nonnegView on Github →