Units

📁 Source: Mathlib/Algebra/Order/Group/Units.lean

Statistics

Metric	Count
Definitions	0
Theorems isOrderedAddMonoid, isOrderedMonoid	2
Total	2

AddUnits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isOrderedAddMonoid 📖	mathematical	—	IsOrderedAddMonoid AddUnits AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid instAddCommGroupAddUnits instPartialOrderAddUnits	—	add_le_add_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono

Units

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isOrderedMonoid 📖	mathematical	—	IsOrderedMonoid Units CommMonoid.toMonoid CommGroup.toCommMonoid instCommGroupUnits instPartialOrderUnits	—	mul_le_mul_left covariant_swap_mul_of_covariant_mul IsOrderedMonoid.toMulLeftMono

---

← Back to Index