small contribution to mathlib?

Stream: new members

[Harold Cooper]

I recently used two variants of docs#function.iterate_succ and docs#function.iterate_succ_supply in some proofs, and thought they might be useful additions to mathlib.

The existing theorems are f^[n.succ] = f^[n] ∘ f and f^[n.succ] x = f^[n] (f x)
(which are trivial / their proofs are both rfl)
…but I needed the swapped versions f^[n.succ] = f ∘ f^[n] and f^[n.succ] x = f (f^[n] x), which I can imagine other people might also find useful.

Anyway if these seem like good additions, could someone give my github username hrldcpr branch write access so I can make a pull request?

(Here's code if it's not clear what I'm talking about:

import data.nat.basic
import logic.function.iterate

universe u

theorem iterate_succ' {α : Type u} (f : α → α) (n : ℕ) :
  f^[n.succ] = f ∘ (f^[n]) :=
begin
  rw [nat.succ_eq_one_add, function.iterate_add],
  refl,
end

theorem iterate_succ_apply' {α : Type u} (f : α → α) (n : ℕ) (x : α) :
  f^[n.succ] x = f (f^[n] x) := by rw iterate_succ'

)

[Kevin Buzzard]

(deleted)

[Kevin Buzzard]

@maintainers

[Mario Carneiro]

pretty sure iterate_succ_apply' already exists

[Mario Carneiro]

The naming system strikes again. It already exists and has that exact name: docs#function.iterate_succ_apply'

[Scott Morrison]

In any case for future use I've sent your invitation to the repo.

[Mario Carneiro]

docs#function.iterate_succ' also exists, again with the same name

[Eric Wieser]

Why are those lemmas in the function namespace when the function in question is nat.iterate?