Star

📁 Source: Mathlib/Algebra/Order/Ring/Star.lean

Statistics

Metric	Count
Definitions	0
Theorems toIsOrderedRing	1
Total	1

StarOrderedRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toIsOrderedRing 📖	mathematical	—	IsOrderedRing CommSemiring.toSemiring	—	toIsOrderedAddMonoid instZeroLEOneClass smul_le_smul_of_nonneg_left IsOrderedModule.toPosSMulMono instIsOrderedModule StarMul.toStarModule IsScalarTower.left smulCommClass_self smul_le_smul_of_nonneg_right IsOrderedModule.toSMulPosMono

---

← Back to Index