Theorem IsStrictlyPositive.sqrt

Modification history

2026-03-19 01:06

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

feat(CStarAlgebra): lemmas related to `CFC.rpow` and `IsStrictlyPositive` (#36784) …

Modified IsStrictlyPositive.sqrt View on Github →

2025-09-26 11:53

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

feat: Define strictly positive operators (i.e. positive definite) (#29087)

Added IsStrictlyPositive.sqrt View on Github →