α : Type u_1
β : Type ?u.1130
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hn : IsFixedPt (f^[n] ∘ f^[m]) x
hm : IsPeriodicPt f m x
⊢ IsPeriodicPt f n x
α : Type u_1
β : Type ?u.1130
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hn : IsPeriodicPt f (n + m) x
hm : IsPeriodicPt f m x
⊢ IsPeriodicPt f n x
rw [IsPeriodicPt, iterate_add] at hn
no goals
α : Type u_1
β : Type ?u.1130
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hn : IsFixedPt (f^[n] ∘ f^[m]) x
hm : IsPeriodicPt f m x
⊢ IsPeriodicPt f n x
exact hn.left_of_comp hm