Theorem CStarAlgebra.rpow_neg_one_le_rpow_neg_one

Modification history

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_oneView on Github →