Commit 2024-09-05 01:57 b1337614

View on Github →

feat: in a C⋆-algebra, b⁻¹ ≤ a⁻¹ ↔ a ≤ b for nonnegative a b : Aˣ (#16364)

Estimated changes

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean

added theorem CFC.conjugate_rpow_neg_one_half

added theorem CStarRing.inv_le_iff

added theorem CStarRing.inv_le_one

added theorem CStarRing.inv_le_one_iff_one_le

added theorem CStarRing.isUnit_of_le

added theorem CStarRing.le_inv_iff

added theorem CStarRing.le_one_of_one_le_inv

added theorem CStarRing.one_le_inv_iff_le_one

added theorem CStarRing.rpow_neg_one_le_one

added theorem CStarRing.rpow_neg_one_le_rpow_neg_one

added theorem le_iff_norm_sqrt_mul_rpow

added theorem le_iff_norm_sqrt_mul_sqrt_inv