Basic

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

Statistics

Metric	Count
Definitions `fib`	1
Theorems `coe_fib_neg`, `fib_add`, `fib_add_one`, `fib_add_two`, `fib_dvd`, `fib_eq_fib_add_two_sub_fib_add_one`, `fib_eq_zero`, `fib_gcd`, `fib_natCast`, `fib_neg`, `fib_neg_natCast`, `fib_neg_one`, `fib_neg_two`, `fib_of_nonneg`, `fib_of_odd`, `fib_one`, `fib_two`, `fib_two_mul`, `fib_two_mul_add_one`, `fib_two_mul_add_one_eq_natFib_natAbs`, `fib_two_mul_add_one_pos`, `fib_two_mul_add_two`, `fib_zero`, `gcd_fib`	24
Total	25

Int

Definitions

Name	Category	Theorems
`fib` 📖	CompOp	27 math math: `fib_succ_mul_fib_pred_sub_fib_sq`, `fib_dvd`, `fib_eq_fib_add_two_sub_fib_add_one`, `fib_neg_natCast`, `fib_zero`, `fib_two_mul_add_one_pos`, `fib_natCast`, `fib_add_one`, `fib_of_nonneg`, `fib_neg_two`, `fib_neg`, `fib_eq_zero`, `Real.coe_intFib_eq`, `fib_one`, `fib_two_mul_add_two`, `fib_two`, `coe_fib_neg`, `fib_two_mul_add_one`, `fib_add`, `fib_two_mul_add_one_eq_natFib_natAbs`, `fib_two_mul`, `fib_of_odd`, `gcd_fib`, `fib_gcd`, `fib_neg_one`, `fib_add_sq_sub_fib_mul_fib_add_two_mul`, `fib_add_two`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_fib_neg` 📖	mathematical	—	`fib`	—	`fib_neg` `neg_one_zpow_eq_ite` `cast_ite` `cast_neg` `ite_mul` `one_mul` `neg_mul`
`fib_add` 📖	mathematical	—	`fib`	—	—
`fib_add_one` 📖	mathematical	—	`fib`	—	`fib_add_two` `add_sub_cancel_left`
`fib_add_two` 📖	mathematical	—	`fib`	—	`Nat.instAtLeastTwoHAddOfNat` `Nat.cast_ofNat` `Nat.cast_add` `Nat.cast_add_one` `fib_natCast` `Nat.fib_add_two` `fib_neg_natCast` `Nat.cast_one` `neg_add_rev` `add_comm` `add_assoc` `add_neg_cancel_comm_assoc` `Nat.cast_zero` `neg_zero` `zero_add` `pow_one` `MulZeroClass.mul_zero` `Even.neg_pow` `one_pow` `mul_one` `Nat.even_or_odd` `Nat.fib_add_one` `pow_add` `two_mul` `Distrib.rightDistribClass` `mul_neg` `sub_add_cancel_right` `neg_mul` `one_mul` `neg_neg` `add_tsub_cancel_right` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid`
`fib_dvd` 📖	mathematical	—	`fib`	—	`fib_neg_natCast`
`fib_eq_fib_add_two_sub_fib_add_one` 📖	mathematical	—	`fib`	—	`fib_add_two` `add_sub_cancel_right`
`fib_eq_zero` 📖	mathematical	—	`fib`	—	`fib_neg_natCast` `IsDomain.to_noZeroDivisors` `instIsDomain` `isReduced_of_noZeroDivisors`
`fib_gcd` 📖	mathematical	—	`fib`	—	`instCharZero` `gcd_fib`
`fib_natCast` 📖	mathematical	—	`fib` `Nat.fib`	—	—
`fib_neg` 📖	mathematical	—	`fib` `Even` `instDecidablePredEven`	—	`fib_neg_natCast` `Even.neg_pow` `one_pow` `one_mul` `Odd.neg_one_pow` `neg_mul` `neg_neg`
`fib_neg_natCast` 📖	mathematical	—	`fib` `Monoid.toNatPow` `instMonoid` `Nat.fib`	—	`Nat.even_or_odd` `Nat.cast_zero` `neg_neg` `pow_add` `Even.neg_pow` `one_pow` `pow_one` `mul_neg` `mul_one` `neg_mul` `one_mul` `fib_of_odd`
`fib_neg_one` 📖	mathematical	—	`fib`	—	—
`fib_neg_two` 📖	mathematical	—	`fib`	—	—
`fib_of_nonneg` 📖	mathematical	—	`fib` `Nat.fib`	—	—
`fib_of_odd` 📖	mathematical	`Odd` `instSemiring`	`fib` `Nat.fib`	—	—
`fib_one` 📖	mathematical	—	`fib`	—	—
`fib_two` 📖	mathematical	—	`fib`	—	—
`fib_two_mul` 📖	mathematical	—	`fib`	—	`Nat.instAtLeastTwoHAddOfNat` `two_mul` `fib_add`
`fib_two_mul_add_one` 📖	mathematical	—	`fib` `Monoid.toNatPow` `instMonoid`	—	`fib_add`
`fib_two_mul_add_one_eq_natFib_natAbs` 📖	mathematical	—	`fib` `Nat.fib`	—	`fib_of_odd` `odd_two_mul_add_one`
`fib_two_mul_add_one_pos` 📖	mathematical	—	`fib`	—	—
`fib_two_mul_add_two` 📖	mathematical	—	`fib`	—	`mul_add_one` `Distrib.leftDistribClass` `fib_two_mul`
`fib_zero` 📖	mathematical	—	`fib`	—	—
`gcd_fib` 📖	mathematical	—	`fib` `Nat.fib`	—	`Nat.fib_gcd` `fib_neg` `apply_ite_left`

---

← Back to Index