Documentation Verification Report

SuccPred

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

Statistics

Metric	Count
Definitions `instPredOrder`, `instPredSubOrder`, `instSuccAddOrder`, `instSuccOrder`	4
Theorems `coe_fin`, `coe_covBy_iff`, `forall_ne_zero_iff`, `instIsPredArchimedean`, `instIsSuccArchimedean`, `le_succ_iff_eq_or_le`, `pred_eq_pred`, `pred_iterate`, `succ_eq_succ`, `succ_iterate`, `withBotSucc_one`, `withBotSucc_zero`	12
Total	16

CovBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_fin` 📖	—	`CovBy`	—	—	`Fin.coe_covBy_iff`

Fin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_covBy_iff` 📖	mathematical	—	`CovBy`	—	`LT.lt.trans` `prop`

Nat

Definitions

Name	Category	Theorems
`instPredOrder` 📖	CompOp	2 math math: `pred_eq_pred`, `instIsPredArchimedean`
`instPredSubOrder` 📖	CompOp	—
`instSuccAddOrder` 📖	CompOp	—
`instSuccOrder` 📖	CompOp	8 math math: `Polynomial.length_coeffList_eq_withBotSucc_degree`, `Polynomial.coeffList_eraseLead`, `succ_eq_succ`, `withBotSucc_zero`, `Ordinal.one_add_natCast`, `instIsSuccArchimedean`, `withBotSucc_one`, `Polynomial.withBotSucc_degree_eq_natDegree_add_one`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`forall_ne_zero_iff` 📖	—	—	—	—	`SuccOrder.forall_ne_bot_iff` `instNontrivial` `instIsSuccArchimedean`
`instIsPredArchimedean` 📖	mathematical	—	`IsPredArchimedean` `instPreorder` `instPredOrder`	—	`pred_eq_pred` `pred_iterate` `tsub_tsub_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le`
`instIsSuccArchimedean` 📖	mathematical	—	`IsSuccArchimedean` `instPreorder` `instSuccOrder`	—	`succ_eq_succ` `succ_iterate` `add_tsub_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `instOrderedSub`
`le_succ_iff_eq_or_le` 📖	—	—	—	—	`Order.le_succ_iff_eq_or_le`
`pred_eq_pred` 📖	mathematical	—	`Order.pred` `instPreorder` `instPredOrder`	—	—
`pred_iterate` 📖	mathematical	—	`iterate`	—	`Function.iterate_succ'`
`succ_eq_succ` 📖	mathematical	—	`Order.succ` `instPreorder` `instSuccOrder`	—	—
`succ_iterate` 📖	mathematical	—	`iterate`	—	`Order.succ_iterate`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`withBotSucc_one` 📖	mathematical	—	`WithBot.succ` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instSuccOrder` `WithBot` `WithBot.one` `Nat.instOne`	—	—
`withBotSucc_zero` 📖	mathematical	—	`WithBot.succ` `Nat.instPreorder` `Nat.instOrderBot` `Nat.instSuccOrder` `WithBot` `WithBot.zero` `MulZeroClass.toZero` `Nat.instMulZeroClass`	—	—

---

← Back to Index