Theorem Units.isStrictlyPositive_of_le

Modification history

2026-03-19 01:06
Mathlib/Algebra/Algebra/StrictPositivity.lean
feat(CStarAlgebra): lemmas related to `CFC.rpow` and `IsStrictlyPositive` (#36784) …
Added Units.isStrictlyPositive_of_leView on Github →