Init

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

Statistics

Metric	Count
Definitions `foundational_algebra_order_theory`, `AtLeastTwo`, `decidableLoHi`, `decidableLoHiLe`, `decreasingInduction`, `decreasingInduction'`, `leRec`, `leRecOn`, `pincerRecursion`, `strongRec'`, `strongRecOn'`, `strongSubRecursion`, `twoStepInduction`	13
Theorems `nat_succ_le`, `neZero_sub_one`, `ne_one`, `one_lt`, `prop`, `toNeZero`, `case_strong_induction_on`, `decreasingInduction_self`, `decreasingInduction_succ`, `decreasingInduction_succ'`, `decreasingInduction_succ_left`, `decreasingInduction_trans`, `diag_induction`, `div_lt_self'`, `dvd_add_self_left`, `dvd_add_self_right`, `dvd_left_iff_eq`, `dvd_right_iff_eq`, `ext_div_mod`, `ext_div_mod_iff`, `forall_lt_succ`, `instAtLeastTwoHAddOfNat`, `instNeZeroNatAbsOfInt_mathlib`, `leRecOn_self`, `leRecOn_succ`, `leRecOn_succ'`, `leRecOn_succ_left`, `leRecOn_trans`, `leRec_eq_leRec`, `leRec_self`, `leRec_succ`, `leRec_succ'`, `leRec_succ_left`, `leRec_trans`, `le_div_two_iff_mul_two_le`, `le_induction`, `mul_def`, `not_pos_pow_dvd`, `not_two_dvd_bit1`, `of_le_succ`, `one_le_pow'`, `rec_add_one`, `rec_one`, `rec_zero`, `sq_sub_sq`, `strongRec'_spec`, `strongRecOn'_beta`, `strong_induction_on`, `succ_pos'`, `two_le_iff`, `two_lt_of_ne`, `two_mul_ne_two_mul_add_one`, `two_mul_odd_div_two`	53
Total	66

LT.lt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nat_succ_le` 📖	—	—	—	—	—

LibraryNote

Definitions

Name	Category	Theorems
`foundational_algebra_order_theory` 📖	CompOp	—

Nat

Definitions

Name	Category	Theorems
`AtLeastTwo` 📖	CompData	2 math math: `instAtLeastTwoHAddOfNat`, `Mathlib.Meta.NormNum.instAtLeastTwo`
`decidableLoHi` 📖	CompOp	—
`decidableLoHiLe` 📖	CompOp	—
`decreasingInduction` 📖	CompOp	5 math math: `decreasingInduction_trans`, `decreasingInduction_self`, `decreasingInduction_succ_left`, `decreasingInduction_succ`, `decreasingInduction_succ'`
`decreasingInduction'` 📖	CompOp	—
`leRec` 📖	CompOp	7 math math: `leRec_trans`, `ProbabilityTheory.Kernel.partialTraj_le_def`, `leRec_succ'`, `leRec_succ_left`, `leRec_eq_leRec`, `leRec_succ`, `leRec_self`
`leRecOn` 📖	CompOp	9 math math: `leRecOn_succ`, `leRecOn_surjective`, `leRecOn_succ'`, `leRecOn_injective`, `leRecOn_trans`, `leRecOn_succ_left`, `leRecOn_self`, `Metric.inductiveLimitDist_eq_dist`, `FirstOrder.Language.DirectedSystem.coe_natLERec`
`pincerRecursion` 📖	CompOp	—
`strongRec'` 📖	CompOp	1 math math: `strongRec'_spec`
`strongRecOn'` 📖	CompOp	1 math math: `strongRecOn'_beta`
`strongSubRecursion` 📖	CompOp	—
`twoStepInduction` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`case_strong_induction_on` 📖	—	—	—	—	—
`decreasingInduction_self` 📖	mathematical	—	`decreasingInduction`	—	`leRec_self`
`decreasingInduction_succ` 📖	mathematical	—	`decreasingInduction`	—	`leRec_succ`
`decreasingInduction_succ'` 📖	mathematical	—	`decreasingInduction`	—	`leRec_succ'`
`decreasingInduction_succ_left` 📖	mathematical	—	`decreasingInduction`	—	`decreasingInduction_trans` `decreasingInduction_succ'`
`decreasingInduction_trans` 📖	mathematical	—	`decreasingInduction`	—	`decreasingInduction_self` `decreasingInduction_succ`
`diag_induction` 📖	—	—	—	—	—
`div_lt_self'` 📖	—	—	—	—	—
`dvd_add_self_left` 📖	—	—	—	—	—
`dvd_add_self_right` 📖	—	—	—	—	—
`dvd_left_iff_eq` 📖	—	—	—	—	—
`dvd_right_iff_eq` 📖	—	—	—	—	—
`ext_div_mod` 📖	—	—	—	—	—
`ext_div_mod_iff` 📖	—	—	—	—	—
`forall_lt_succ` 📖	—	—	—	—	—
`instAtLeastTwoHAddOfNat` 📖	mathematical	—	`AtLeastTwo`	—	—
`instNeZeroNatAbsOfInt_mathlib` 📖	—	—	—	—	—
`leRecOn_self` 📖	mathematical	—	`leRecOn`	—	`leRec_self`
`leRecOn_succ` 📖	mathematical	—	`leRecOn`	—	`leRec_succ`
`leRecOn_succ'` 📖	mathematical	—	`leRecOn`	—	`leRec_succ'`
`leRecOn_succ_left` 📖	mathematical	—	`leRecOn`	—	`leRec_succ_left`
`leRecOn_trans` 📖	mathematical	—	`leRecOn`	—	`leRec_trans`
`leRec_eq_leRec` 📖	mathematical	—	`leRec`	—	—
`leRec_self` 📖	mathematical	—	`leRec`	—	—
`leRec_succ` 📖	mathematical	—	`leRec`	—	`leRec.eq_2` `Or.by_cases.eq_1`
`leRec_succ'` 📖	mathematical	—	`leRec`	—	`leRec_succ` `leRec_self`
`leRec_succ_left` 📖	mathematical	—	`leRec`	—	`leRec_trans` `leRec_succ'`
`leRec_trans` 📖	mathematical	—	`leRec`	—	`leRec_self` `leRec_succ`
`le_div_two_iff_mul_two_le` 📖	—	—	—	—	—
`le_induction` 📖	—	—	—	—	—
`mul_def` 📖	—	—	—	—	—
`not_pos_pow_dvd` 📖	—	—	—	—	—
`not_two_dvd_bit1` 📖	—	—	—	—	—
`of_le_succ` 📖	—	—	—	—	—
`one_le_pow'` 📖	—	—	—	—	—
`rec_add_one` 📖	—	—	—	—	—
`rec_one` 📖	—	—	—	—	—
`rec_zero` 📖	—	—	—	—	—
`sq_sub_sq` 📖	—	—	—	—	—
`strongRec'_spec` 📖	mathematical	—	`strongRec'`	—	—
`strongRecOn'_beta` 📖	mathematical	—	`strongRecOn'`	—	`strongRec'_spec`
`strong_induction_on` 📖	—	—	—	—	—
`succ_pos'` 📖	—	—	—	—	—
`two_le_iff` 📖	—	—	—	—	—
`two_lt_of_ne` 📖	—	—	—	—	—
`two_mul_ne_two_mul_add_one` 📖	—	—	—	—	—
`two_mul_odd_div_two` 📖	—	—	—	—	—

Nat.AtLeastTwo

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`neZero_sub_one` 📖	—	—	—	—	`prop`
`ne_one` 📖	—	—	—	—	`one_lt`
`one_lt` 📖	—	—	—	—	`prop`
`prop` 📖	—	—	—	—	—
`toNeZero` 📖	—	—	—	—	`one_lt`

---

← Back to Index