WithBot

📁 Source: Mathlib/Data/Nat/WithBot.lean

Statistics

Metric	Count
Definitions instWellFoundedRelationWithBot	1
Theorems add_eq_one_iff, add_eq_three_iff, add_eq_two_iff, add_eq_zero_iff, add_one_le_of_lt, coe_nonneg, lt_one_iff_le_zero, lt_zero_iff, one_le_iff_zero_lt	9
Total	10

Nat.WithBot

Definitions

Name	Category	Theorems
instWellFoundedRelationWithBot 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_eq_one_iff 📖	mathematical	—	WithBot WithBot.add WithBot.one Nat.instOne WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass	—	WithBot.add_bot
add_eq_three_iff 📖	mathematical	—	WithBot WithBot.add instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass WithBot.one Nat.instOne	—	Nat.instAtLeastTwoHAddOfNat WithBot.add_bot
add_eq_two_iff 📖	mathematical	—	WithBot WithBot.add instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass WithBot.one Nat.instOne	—	Nat.instAtLeastTwoHAddOfNat WithBot.add_bot
add_eq_zero_iff 📖	mathematical	—	WithBot WithBot.add WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass	—	WithBot.add_bot
add_one_le_of_lt 📖	mathematical	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder	Preorder.toLE WithBot.add WithBot.one Nat.instOne	—	not_lt_bot WithBot.coe_one WithBot.coe_add WithBot.coe_le_coe WithBot.coe_lt_coe
coe_nonneg 📖	mathematical	—	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne	—	WithBot.coe_zero Nat.cast_withBot WithBot.coe_le_coe
lt_one_iff_le_zero 📖	mathematical	—	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder WithBot.one Nat.instOne Preorder.toLE WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass	—	not_iff_not one_le_iff_zero_lt
lt_zero_iff 📖	mathematical	—	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass Bot.bot WithBot.bot	—	WithBot.lt_coe_bot
one_le_iff_zero_lt 📖	mathematical	—	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder WithBot.one Nat.instOne Preorder.toLT WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass	—	LT.lt.trans_le zero_lt_one WithBot.zeroLEOneClass Nat.instZeroLEOneClass NeZero.charZero_one WithBot.charZero Nat.instCharZero not_lt_bot WithBot.coe_one WithBot.coe_le_coe zero_add WithBot.coe_lt_coe WithBot.coe_zero

---

← Back to Index