Theorem cfc_nonneg_of_predicate

Modification history

2025-03-05 06:23
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
feat: generalize order typeclasses (#22569) …
Modified cfc_nonneg_of_predicateView on Github →
2024-09-02 17:15
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
feat(ContinuousFunctionalCalculus): add lemmas for automation and simp/aesop tags (#16050) …
Added cfc_nonneg_of_predicateView on Github →