Nat

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

Statistics

Metric	Count
Definitions	0
Theorems instCanonicallyOrderedAdd, instIsOrderedAddMonoid, instIsOrderedCancelAddMonoid, instOrderedSub, pow_left_strictMono, nat_pow	6
Total	6

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instCanonicallyOrderedAdd 📖	mathematical	—	CanonicallyOrderedAdd	—	—
instIsOrderedAddMonoid 📖	mathematical	—	IsOrderedAddMonoid instAddCommMonoid instPartialOrder	—	—
instIsOrderedCancelAddMonoid 📖	mathematical	—	IsOrderedCancelAddMonoid instAddCommMonoid instPartialOrder	—	—
instOrderedSub 📖	mathematical	—	OrderedSub	—	add_zero
pow_left_strictMono 📖	mathematical	—	StrictMono instPreorder Monoid.toNatPow instMonoid	—	—

StrictMono

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nat_pow 📖	mathematical	StrictMono Nat.instPreorder	Monoid.toNatPow Nat.instMonoid	—	comp Nat.pow_left_strictMono

---

← Back to Index