Basic

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

Statistics

Metric	Count
Definitions fastFib, fastFibAux, fib	3
Theorems fastFibAux_bit_false, fastFibAux_bit_true, fastFibAux_eq, fastFib_eq, fast_fib_aux_bit_ff, fast_fib_aux_bit_tt, fast_fib_aux_eq, fast_fib_eq, fib_add, fib_add_one, fib_add_two, fib_add_two_strictMono, fib_add_two_sub_fib_add_one, fib_coprime_fib_succ, fib_dvd, fib_eq_fastFib, fib_eq_zero, fib_gcd, fib_le_fib_succ, fib_lt_fib, fib_lt_fib_succ, fib_mono, fib_one, fib_pos, fib_strictMonoOn, fib_succ_eq_succ_sum, fib_succ_eq_sum_choose, fib_two, fib_two_mul, fib_two_mul_add_one, fib_two_mul_add_two, fib_zero, gcd_fib_add_mul_self, gcd_fib_add_self, le_fib_add_one, le_fib_self	36
Total	39

Nat

Definitions

Name	Category	Theorems
fastFib 📖	CompOp	3 math math: fastFib_eq, fib_eq_fastFib, fast_fib_eq
fastFibAux 📖	CompOp	6 math math: fast_fib_aux_bit_ff, fast_fib_aux_eq, fast_fib_aux_bit_tt, fastFibAux_bit_false, fastFibAux_eq, fastFibAux_bit_true
fib 📖	CompOp	64 math math: fastFib_eq, Real.goldenConj_mul_fib_succ_add_fib, lt_fib_greatestFib_add_one, greatestFib_fib, fib_le_fib_succ, GenContFract.succ_nth_fib_le_of_nth_den, Int.fib_neg_natCast, fib_coprime_fib_succ, fast_fib_aux_eq, fib_lt_fib_succ, Mathlib.Meta.NormNum.isFibAux_two_mul_add_one_done, fib_add_two_sub_fib_add_one, fib_golden_exp', Int.fib_natCast, fib_mono, Real.coe_fib_eq, greatestFib_lt, fib_succ_eq_succ_sum, fib_add_two, Int.fib_of_nonneg, fib_gcd, List.IsZeckendorfRep.sum_fib_lt, fib_dvd, Real.goldenRatio_mul_fib_succ_add_fib, fib_two_mul, fib_pos, fib_eq_fastFib, tendsto_fib_div_fib_succ_atTop, fib_greatestFib_le, fib_lt_fib, greatestFib_sub_fib_greatestFib_le_greatestFib, fib_two_mul_add_one, gcd_fib_add_self, fib_one, fib_strictMonoOn, fib_two, Real.coe_fib_eq', sum_zeckendorf_fib, Real.fib_isSol_fibRec, fib_add_two_strictMono, GenContFract.fib_le_of_contsAux_b, fib_two_mul_add_two, fib_add, fib_golden_conj_exp, fast_fib_eq, fib_succ_eq_sum_choose, le_fib_self, zeckendorf_succ, Int.fib_two_mul_add_one_eq_natFib_natAbs, tendsto_fib_succ_div_fib_atTop, fib_zero, zeckendorf_of_pos, fib_eq_zero, fastFibAux_eq, le_greatestFib, Real.fib_succ_sub_goldenConj_mul_fib, Int.fib_of_odd, le_fib_add_one, Real.fib_succ_sub_goldenRatio_mul_fib, fib_add_one, Int.gcd_fib, gcd_fib_add_mul_self, Mathlib.Meta.NormNum.isFibAux_two_mul_done, zeckendorf_sum_fib

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fastFibAux_bit_false 📖	mathematical	—	fastFibAux bit	—	fastFibAux.eq_1 binaryRec_eq mul_one tsub_zero instOrderedSub MulZeroClass.zero_mul one_pow zero_pow instCharZero instAtLeastTwoHAddOfNat add_zero
fastFibAux_bit_true 📖	mathematical	—	fastFibAux bit	—	fastFibAux.eq_1 binaryRec_eq mul_one tsub_zero instOrderedSub MulZeroClass.zero_mul one_pow zero_pow instCharZero instAtLeastTwoHAddOfNat add_zero
fastFibAux_eq 📖	mathematical	—	fastFibAux fib	—	zero_add fastFibAux_bit_false fib_two_mul fib_two_mul_add_one fastFibAux_bit_true fib_two_mul_add_two
fastFib_eq 📖	mathematical	—	fastFib fib	—	fastFib.eq_1 fastFibAux_eq
fast_fib_aux_bit_ff 📖	mathematical	—	fastFibAux bit	—	fastFibAux_bit_false
fast_fib_aux_bit_tt 📖	mathematical	—	fastFibAux bit	—	fastFibAux_bit_true
fast_fib_aux_eq 📖	mathematical	—	fastFibAux fib	—	fastFibAux_eq
fast_fib_eq 📖	mathematical	—	fastFib fib	—	fastFib_eq
fib_add 📖	mathematical	—	fib	—	add_zero MulZeroClass.mul_zero zero_add mul_one add_comm add_assoc fib_add_two Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add
fib_add_one 📖	mathematical	—	fib	—	fib_add_two
fib_add_two 📖	mathematical	—	fib	—	Function.iterate_succ_apply'
fib_add_two_strictMono 📖	mathematical	—	StrictMono instPreorder fib	—	strictMono_nat_of_lt_succ add_right_comm fib_lt_fib_succ self_le_add_left instCanonicallyOrderedAdd
fib_add_two_sub_fib_add_one 📖	mathematical	—	fib	—	fib_add_two add_tsub_cancel_right instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid
fib_coprime_fib_succ 📖	mathematical	—	fib	—	zero_add fib_add_two
fib_dvd 📖	mathematical	—	fib	—	fib_gcd
fib_eq_fastFib 📖	mathematical	—	fib fastFib	—	fastFib_eq
fib_eq_zero 📖	mathematical	—	fib	—	fib_add_two instCharZero instAtLeastTwoHAddOfNat
fib_gcd 📖	mathematical	—	fib	—	gcd_fib_add_mul_self
fib_le_fib_succ 📖	mathematical	—	fib	—	zero_add instCanonicallyOrderedAdd fib_add_two covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le
fib_lt_fib 📖	mathematical	—	fib	—	instCanonicallyOrderedAdd StrictMonoOn.lt_iff_lt fib_strictMonoOn covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le
fib_lt_fib_succ 📖	mathematical	—	fib	—	ExistsAddOfLE.exists_add_of_le CanonicallyOrderedAdd.toExistsAddOfLE instCanonicallyOrderedAdd tsub_pos_iff_lt instOrderedSub add_comm add_right_comm fib_add_two add_tsub_cancel_right IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid fib_pos
fib_mono 📖	mathematical	—	Monotone instPreorder fib	—	monotone_nat_of_le_succ fib_le_fib_succ
fib_one 📖	mathematical	—	fib	—	—
fib_pos 📖	mathematical	—	fib	—	instCanonicallyOrderedAdd
fib_strictMonoOn 📖	mathematical	—	StrictMonoOn instPreorder fib Set.Ici	—	fib_add_two_strictMono lt_of_add_lt_add_right contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid
fib_succ_eq_succ_sum 📖	mathematical	—	fib Finset.sum instAddCommMonoid Finset.range	—	zero_add fib_add_two add_assoc Finset.sum_congr Finset.range_add_one Finset.sum_insert
fib_succ_eq_sum_choose 📖	mathematical	—	fib Finset.sum instAddCommMonoid Finset.HasAntidiagonal.antidiagonal instAddMonoid Finset.Nat.instHasAntidiagonal choose	—	fib_add_two succ_injective Finset.Nat.antidiagonal_succ_succ' Finset.Nat.antidiagonal_succ' Finset.sum_congr Finset.cons_eq_insert Finset.sum_insert choose_zero_right Finset.sum_map add_left_comm Finset.cons.congr_simp instCharZero instAtLeastTwoHAddOfNat Finset.sum_add_distrib zero_add
fib_two 📖	mathematical	—	fib	—	—
fib_two_mul 📖	mathematical	—	fib	—	MulZeroClass.mul_zero zero_add mul_one tsub_zero instOrderedSub MulZeroClass.zero_mul instAtLeastTwoHAddOfNat two_mul add_assoc fib_add fib_add_two add_tsub_cancel_right IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_lt
fib_two_mul_add_one 📖	mathematical	—	fib Monoid.toNatPow instMonoid	—	instAtLeastTwoHAddOfNat two_mul fib_add Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.add_pf_add_gt
fib_two_mul_add_two 📖	mathematical	—	fib	—	fib_add_two fib_two_mul fib_two_mul_add_one le_trans fib_le_fib_succ two_pos instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid mul_comm instAtLeastTwoHAddOfNat cast_add cast_mul cast_sub cast_pow Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add
fib_zero 📖	mathematical	—	fib	—	—
gcd_fib_add_mul_self 📖	mathematical	—	fib	—	MulZeroClass.zero_mul add_zero add_mul Distrib.rightDistribClass add_assoc one_mul gcd_fib_add_self
gcd_fib_add_self 📖	mathematical	—	fib	—	zero_add fib_add Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one add_zero Mathlib.Tactic.RingNF.add_assoc_rev add_comm fib_coprime_fib_succ
le_fib_add_one 📖	mathematical	—	fib	—	zero_le_one instZeroLEOneClass one_le_two IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid le_rfl LE.le.trans le_fib_self le_add_self instCanonicallyOrderedAdd
le_fib_self 📖	mathematical	—	fib	—	le_refl fib_lt_fib_succ le_trans

---

← Back to Index