Theorem IsSelfAdjoint.exp_nonneg

Modification history

2026-01-06 16:13

Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog/Basic.lean

refactor(Analysis/NormedSpace/Exponential): remove the `𝕂` argument from `exp` (#30706) …

Modified IsSelfAdjoint.exp_nonneg View on Github →

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_nonneg View on Github →