Theorem CStarAlgebra.rpow_neg_one_le_rpow_neg_one

Modification history

2025-11-04 20:27

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean

chore(Analysis/CStarAlgebra/CFC/Order): relate section to strict positivity (#30694)

Modified CStarAlgebra.rpow_neg_one_le_rpow_neg_one View on Github →

2024-09-12 16:24

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean

chore: namespace lemmas to `CStarAlgebra` instead of `CStarRing` (#16653) …

Added CStarAlgebra.rpow_neg_one_le_rpow_neg_one View on Github →