Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-29 17:49 fcbe7142

View on Github →

refactor(data/nat/fib): use nat.iterate (#10489) The main drawback of the new definition is that fib (n + 2) = fib n + fib (n + 1) is no longer rfl but I think that we should have one API for iterates. See discussion at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60nat.2Eiterate.60.20vs.20.60stream.2Eiterate.60

Estimated changes

modified def nat.fib
added theorem nat.fib_add_two
modified theorem nat.fib_le_fib_succ
added theorem nat.fib_lt_fib_succ
deleted theorem nat.fib_succ_succ
modified theorem nat.gcd_add_mul_self
added theorem nat.gcd_add_self_left
added theorem nat.gcd_add_self_right
modified theorem nat.gcd_eq_zero_iff
added theorem nat.gcd_self_add_left
added theorem nat.gcd_self_add_right