NatFib

📁 Source: Mathlib/Tactic/NormNum/NatFib.lean

Statistics

Metric	Count
Definitions IsFibAux, evalNatFib, proveNatFib, proveNatFibAux	4
Theorems isFibAux_one, isFibAux_two_mul, isFibAux_two_mul_add_one, isFibAux_two_mul_add_one_done, isFibAux_two_mul_done, isFibAux_zero, isNat_fib	7
Total	11

Mathlib.Meta.NormNum

Definitions

Name	Category	Theorems
IsFibAux 📖	MathDef	2 math math: isFibAux_zero, isFibAux_one
evalNatFib 📖	CompOp	—
proveNatFib 📖	CompOp	—
proveNatFibAux 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isFibAux_one 📖	mathematical	—	IsFibAux	—	Nat.fib_one Nat.fib_two
isFibAux_two_mul 📖	—	IsFibAux	—	—	Nat.fib_two_mul Nat.fib_two_mul_add_one pow_two add_comm
isFibAux_two_mul_add_one 📖	—	IsFibAux	—	—	Nat.fib_two_mul_add_one pow_two add_comm Nat.fib_two_mul_add_two
isFibAux_two_mul_add_one_done 📖	mathematical	IsFibAux	Nat.fib	—	isFibAux_two_mul_add_one
isFibAux_two_mul_done 📖	mathematical	IsFibAux	Nat.fib	—	isFibAux_two_mul
isFibAux_zero 📖	mathematical	—	IsFibAux	—	Nat.fib_zero Nat.fib_one
isNat_fib 📖	—	IsNat Nat.instAddMonoidWithOne Nat.fib	—	—	—

---

← Back to Index