Documentation Verification Report

Zeckendorf

📁 Source: Mathlib/Data/Nat/Fib/Zeckendorf.lean

Statistics

Metric	Count
Definitions `IsZeckendorfRep`, `greatestFib`, `zeckendorf`, `zeckendorfEquiv`	4
Theorems `sum_fib_lt`, `IsZeckendorfRep_nil`, `fib_greatestFib_le`, `greatestFib_eq_zero`, `greatestFib_fib`, `greatestFib_lt`, `greatestFib_mono`, `greatestFib_ne_zero`, `greatestFib_pos`, `greatestFib_sub_fib_greatestFib_le_greatestFib`, `isZeckendorfRep_zeckendorf`, `le_greatestFib`, `lt_fib_greatestFib_add_one`, `sum_zeckendorf_fib`, `zeckendorf_of_pos`, `zeckendorf_succ`, `zeckendorf_sum_fib`, `zeckendorf_zero`, `instIsTransNatLeHAddOfNat`	19
Total	23

List

Definitions

Name	Category	Theorems
`IsZeckendorfRep` 📖	MathDef	2 math math: `IsZeckendorfRep_nil`, `Nat.isZeckendorfRep_zeckendorf`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`IsZeckendorfRep_nil` 📖	mathematical	—	`IsZeckendorfRep`	—	—

List.IsZeckendorfRep

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sum_fib_lt` 📖	mathematical	`List.IsZeckendorfRep`	`MulZeroClass.toZero` `Nat.instMulZeroClass` `Nat.fib`	—	`Nat.fib_pos` `lt_tsub_iff_right` `Nat.instOrderedSub` `instIsTransNatLeHAddOfNat` `add_lt_add_right` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `zero_add` `add_comm` `Nat.fib_add_one` `LT.lt.ne'` `LE.le.trans_lt'` `zero_lt_two` `Nat.instZeroLEOneClass` `Nat.fib_mono`

Nat

Definitions

Name	Category	Theorems
`greatestFib` 📖	CompOp	11 math math: `greatestFib_pos`, `lt_fib_greatestFib_add_one`, `greatestFib_fib`, `greatestFib_lt`, `greatestFib_eq_zero`, `fib_greatestFib_le`, `greatestFib_sub_fib_greatestFib_le_greatestFib`, `zeckendorf_succ`, `zeckendorf_of_pos`, `le_greatestFib`, `greatestFib_mono`
`zeckendorf` 📖	CompOp	6 math math: `zeckendorf_zero`, `isZeckendorfRep_zeckendorf`, `sum_zeckendorf_fib`, `zeckendorf_succ`, `zeckendorf_of_pos`, `zeckendorf_sum_fib`
`zeckendorfEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fib_greatestFib_le` 📖	mathematical	—	`fib` `greatestFib`	—	`findGreatest_spec`
`greatestFib_eq_zero` 📖	mathematical	—	`greatestFib`	—	`findGreatest_eq_zero_iff` `zero_lt_one` `instZeroLEOneClass` `le_add_self` `instCanonicallyOrderedAdd`
`greatestFib_fib` 📖	mathematical	—	`greatestFib` `fib`	—	`findGreatest_eq_iff` `le_fib_add_one` `le_rfl` `LT.lt.not_ge` `fib_lt_fib` `le_add_self` `instCanonicallyOrderedAdd`
`greatestFib_lt` 📖	mathematical	—	`greatestFib` `fib`	—	`lt_iff_lt_of_le_iff_le` `le_greatestFib`
`greatestFib_mono` 📖	mathematical	—	`Monotone` `instPreorder` `greatestFib`	—	`findGreatest_mono` `LE.le.trans'` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid`
`greatestFib_ne_zero` 📖	—	—	—	—	`Iff.not` `greatestFib_eq_zero`
`greatestFib_pos` 📖	mathematical	—	`greatestFib`	—	`instCanonicallyOrderedAdd`
`greatestFib_sub_fib_greatestFib_le_greatestFib` 📖	mathematical	—	`greatestFib` `fib`	—	`greatestFib_lt` `tsub_lt_iff_right` `CanonicallyOrderedAdd.toExistsAddOfLE` `instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `fib_greatestFib_le` `zero_add` `Ne.bot_lt` `fib_add_one` `lt_fib_greatestFib_add_one`
`isZeckendorfRep_zeckendorf` 📖	mathematical	—	`List.IsZeckendorfRep` `zeckendorf`	—	`zeckendorf_zero` `zeckendorf_succ` `List.IsZeckendorfRep.eq_1` `List.IsChain.cons` `instCanonicallyOrderedAdd` `instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `instZeroLEOneClass` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `contravariant_swap_add_of_contravariant_add` `le_greatestFib` `le_add_self` `add_le_of_le_tsub_right_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `greatestFib_sub_fib_greatestFib_le_greatestFib` `zeckendorf_of_pos`
`le_greatestFib` 📖	mathematical	—	`greatestFib` `fib`	—	`LE.le.trans` `fib_mono` `fib_greatestFib_le` `le_findGreatest` `le_fib_add_one` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid`
`lt_fib_greatestFib_add_one` 📖	mathematical	—	`fib` `greatestFib`	—	`greatestFib_lt`
`sum_zeckendorf_fib` 📖	mathematical	—	`MulZeroClass.toZero` `instMulZeroClass` `fib` `zeckendorf`	—	`zeckendorf.induct` `zeckendorf_zero` `zeckendorf_succ` `add_tsub_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `instOrderedSub`
`zeckendorf_of_pos` 📖	mathematical	—	`zeckendorf` `greatestFib` `fib`	—	`zeckendorf_succ`
`zeckendorf_succ` 📖	mathematical	—	`zeckendorf` `greatestFib` `fib`	—	`zeckendorf.eq_2`
`zeckendorf_sum_fib` 📖	mathematical	`List.IsZeckendorfRep`	`zeckendorf` `MulZeroClass.toZero` `instMulZeroClass` `fib`	—	`zeckendorf_zero` `LE.le.trans_lt'` `instIsTransNatLeHAddOfNat` `zero_add` `zero_lt_two` `instZeroLEOneClass` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `findGreatest.congr_simp` `add_comm` `add_assoc` `LT.lt.ne'` `covariant_swap_add_of_covariant_add` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `instCanonicallyOrderedAdd` `le_add_of_le_right` `le_fib_add_one` `List.IsZeckendorfRep.sum_fib_lt` `zeckendorf_of_pos` `fib_pos` `add_tsub_cancel_left` `instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd`
`zeckendorf_zero` 📖	mathematical	—	`zeckendorf`	—	`zeckendorf.eq_1`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsTransNatLeHAddOfNat` 📖	mathematical	—	`IsTrans`	—	`LE.le.trans` `le_self_add` `Nat.instCanonicallyOrderedAdd`

---

← Back to Index