Commit 2026-03-19 01:06 9abae7f3

View on Github →

feat(CStarAlgebra): lemmas related to CFC.rpow and IsStrictlyPositive (#36784) This PR adds a few lemmas related to CFC.rpow for strictly positive elements. Furthermore, it adjusts the arguments of several existing lemmas now that IsStrictlyPositive exists, and adds autoparams where appropriate. (I don't think it makes sense to add deprecations here: we really want to keep the same lemma names, and it should be fairly easy to adjust downstream code.)

Estimated changes

Modified Mathlib/Algebra/Algebra/StrictPositivity.lean

added theorem Units.isStrictlyPositive_iff

added theorem Units.isStrictlyPositive_of_le

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

Modified Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean

added theorem CFC.inverse_eq_rpow_neg_one

added theorem CFC.inverse_rpow

modified theorem CFC.rpow_mul_rpow_neg

modified theorem CFC.rpow_neg_mul_rpow

modified theorem IsStrictlyPositive.nnrpow

modified theorem IsStrictlyPositive.rpow

modified theorem IsStrictlyPositive.sqrt