Commit 2026-04-01 16:05 a9dd44d9

View on Github →

feat(CStarAlgebra): Ring.inverse is convex and antitone on strictly positive operators (#37009) This PR shows that the inverse is operator convex and operator antitone (we had the latter for inverse of elements in Units, but not for Ring.inverse).

Estimated changes

added theorem IsUnit.mul_left_iff
added theorem IsUnit.mul_right_iff
modified theorem Ring.inverse_inverse
added theorem Ring.inverse_mul
added theorem CFC.cfc_rpow
added theorem CFC.sqrt_of_not_nonneg
added theorem CFC.sqrt_ringInverse
deleted theorem IsUnit.cfcSqrt
added theorem CFC.conjSqrt_apply
added theorem CFC.conjSqrt_monotone
added theorem CFC.conjSqrt_one