StarOrdered

📁 Source: Mathlib/Data/Real/StarOrdered.lean

Statistics

Metric	Count
Definitions	0
Theorems instStarOrderedRing, instStarOrderedRing	2
Total	2

NNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instStarOrderedRing 📖	mathematical	—	StarOrderedRing NNReal NonUnitalCommSemiring.toNonUnitalSemiring CommSemiring.toNonUnitalCommSemiring instCommSemiringNNReal instPartialOrderNNReal instStarRingNNReal	—	StarOrderedRing.of_le_iff ExistsAddOfLE.exists_add_of_le CanonicallyOrderedAdd.toExistsAddOfLE instCanonicallyOrderedAdd TrivialStar.star_trivial instTrivialStarNNReal mul_self_sqrt le_self_add

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instStarOrderedRing 📖	mathematical	—	StarOrderedRing Real NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing commRing partialOrder instStarRingReal	—	StarOrderedRing.of_nonneg_iff' add_le_add_right IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid mul_self_sqrt mul_self_nonneg AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono instIsOrderedRing

---

← Back to Index