Commit 2024-09-02 17:15 f215b3b2
View on Github →feat(ContinuousFunctionalCalculus): add lemmas for automation and simp/aesop tags (#16050)
This PR adds various aesop tags related to the continuous functional calculus. It also introduces the specialized aesop ruleset CFC for lemmas that would be unsuitable for the default ruleset.
It also adds a proof that the exponential of a self-adjoint operator is positive.