Theorem CFC.conjugate_rpow_neg_one_half

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 CFC.conjugate_rpow_neg_one_halfView on Github →
2024-09-05 01:57
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
feat: in a C⋆-algebra, `b⁻¹ ≤ a⁻¹ ↔ a ≤ b` for nonnegative `a b : Aˣ` (#16364)
Added CFC.conjugate_rpow_neg_one_halfView on Github →