Theorem IsUnit.cfcSqrt

Modification history

2026-04-01 16:05

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

feat(CStarAlgebra): `Ring.inverse` is convex and antitone on strictly positive operators (#37009) …

Deleted IsUnit.cfcSqrt View on Github →

2025-06-04 02:56

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

feat(ContinuousFunctionalCalculus): `a ^ y` is invertible iff `a` is invertible (#25005) …

Added IsUnit.cfcSqrt View on Github →