Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-21 07:51 951b967d

View on Github →

refactor(data/nat/basic): use function equality for iterate lemmas (#2748)

Estimated changes

Modified src/algebra/group_power.lean

Modified src/analysis/calculus/deriv.lean

Modified src/analysis/normed_space/banach.lean

Modified src/analysis/special_functions/exp_log.lean

Modified src/computability/turing_machine.lean

Modified src/data/nat/basic.lean

modified theorem nat.iterate_add

added theorem nat.iterate_add_apply

modified theorem nat.iterate_succ'

modified theorem nat.iterate_succ

added theorem nat.iterate_succ_apply'

added theorem nat.iterate_succ_apply

modified theorem nat.iterate_zero

added theorem nat.iterate_zero_apply

Modified src/field_theory/perfect_closure.lean

Modified src/topology/metric_space/contracting.lean