Documentation Verification Report

NatCast

📁 Source: Mathlib/Algebra/Order/Monoid/NatCast.lean

Statistics

Metric	Count
Definitions	0
Theorems `four`, `three`, `two`, `four_pos`, `lt_add_one`, `lt_one_add`, `one_le_two`, `one_le_two'`, `one_lt_two`, `three_pos`, `two_pos`, `zero_le_four`, `zero_le_three`, `zero_le_two`, `zero_lt_four`, `zero_lt_four'`, `zero_lt_three`, `zero_lt_three'`, `zero_lt_two`, `zero_lt_two'`	20
Total	20

ZeroLEOneClass.neZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`four` 📖	mathematical	—	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `LT.lt.ne'` `zero_lt_four`
`three` 📖	mathematical	—	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `LT.lt.ne'` `zero_lt_three`
`two` 📖	mathematical	—	`AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `LT.lt.ne'` `zero_lt_two`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`four_pos` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`zero_lt_four`
`lt_add_one` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `AddZero.toAdd` `AddZeroClass.toAddZero`	—	`lt_add_of_pos_right` `zero_lt_one`
`lt_one_add` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `AddZero.toAdd` `AddZeroClass.toAddZero`	—	`lt_add_of_pos_left` `zero_lt_one`
`one_le_two` 📖	mathematical	—	`AddMonoidWithOne.toOne` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `add_zero` `add_le_add_right` `zero_le_one` `one_add_one_eq_two`
`one_le_two'` 📖	mathematical	—	`AddMonoidWithOne.toOne` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `zero_add` `add_le_add_left` `zero_le_one` `one_add_one_eq_two`
`one_lt_two` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `AddMonoidWithOne.toOne` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `one_add_one_eq_two` `lt_add_one`
`three_pos` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`zero_lt_three`
`two_pos` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`zero_lt_two`
`zero_le_four` 📖	mathematical	—	`Preorder.toLE` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `three_add_one_eq_four` `add_nonneg` `zero_le_three` `zero_le_one`
`zero_le_three` 📖	mathematical	—	`Preorder.toLE` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `two_add_one_eq_three` `add_nonneg` `zero_le_two` `zero_le_one`
`zero_le_two` 📖	mathematical	—	`Preorder.toLE` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `one_add_one_eq_two` `add_nonneg` `zero_le_one`
`zero_lt_four` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `three_add_one_eq_four` `lt_add_of_lt_of_nonneg` `zero_lt_three` `zero_le_one`
`zero_lt_four'` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`zero_lt_four`
`zero_lt_three` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `two_add_one_eq_three` `lt_add_of_lt_of_nonneg` `zero_lt_two` `zero_le_one`
`zero_lt_three'` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`zero_lt_three`
`zero_lt_two` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`LT.lt.trans_le` `Nat.instAtLeastTwoHAddOfNat` `zero_lt_one` `one_le_two`
`zero_lt_two'` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`zero_lt_two`

---

← Back to Index