Theorem CStarRing.inv_le_one_iff_one_le

Modification history

2024-09-12 16:24

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean

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

Deleted CStarRing.inv_le_one_iff_one_le View 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.inv_le_one_iff_one_le View on Github →