α : Type u_1
β : Type ?u.2806
f fa : α → α
fb : β → β
x y : α
m✝ n : ℕ
hf : IsPeriodicPt f n x
m : ℕ
⊢ IsFixedPt (f^[n]^[m]) x
α : Type u_1
β : Type ?u.2806
f fa : α → α
fb : β → β
x y : α
m✝ n : ℕ
hf : IsPeriodicPt f n x
m : ℕ
⊢ IsPeriodicPt (f^[m]) n x
rw [IsPeriodicPt, ← iterate_mul, mul_comm, iterate_mul]
no goals
α : Type u_1
β : Type ?u.2806
f fa : α → α
fb : β → β
x y : α
m✝ n : ℕ
hf : IsPeriodicPt f n x
m : ℕ
⊢ IsFixedPt (f^[n]^[m]) x
exact hf.isFixedPt.iterate m