Prod

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

Statistics

Metric	Count
Definitions	0
Theorems instStarOrderedRing	1
Total	1

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instStarOrderedRing 📖	mathematical	—	StarOrderedRing instNonUnitalSemiring instPartialOrder instStarRing NonUnitalSemiring.toNonUnitalNonAssocSemiring	—	AddSubmonoid.closure_prod Set.mem_range star_zero MulZeroClass.mul_zero Set.prod_range_range_eq

---

← Back to Index