α : Type u
β : Type v
f : α → α
m n : ℕ
x : α
⊢ (f^[m] ∘ f^[n]) x = (f^[m]) ((f^[n]) x)
α : Type u
β : Type v
f : α → α
m n : ℕ
x : α
⊢ (f^[m + n]) x = (f^[m]) ((f^[n]) x)
rw [iterate_add f m n]
no goals
α : Type u
β : Type v
f : α → α
m n : ℕ
x : α
⊢ (f^[m] ∘ f^[n]) x = (f^[m]) ((f^[n]) x)
rfl