Theorem conjugate_nonneg_of_nonneg

Modification history

2024-09-02 17:15

Mathlib/Algebra/Star/Order.lean

feat(ContinuousFunctionalCalculus): add lemmas for automation and simp/aesop tags (#16050) …

Added conjugate_nonneg_of_nonneg View on Github →