Theorem CStarRing.rpow_neg_one_le_one

Modification history

2024-09-12 16:24
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
chore: namespace lemmas to `CStarAlgebra` instead of `CStarRing` (#16653) …
Deleted CStarRing.rpow_neg_one_le_oneView 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 CStarRing.rpow_neg_one_le_oneView on Github →