α : Type u_1
β : Type ?u.3348
f fa : α → α
fb : β → β
x y : α
m n : ℕ
g : α → α
hco : Commute f g
hfg : IsFixedPt (f^[n] ∘ g^[n]) x
hg : IsPeriodicPt g n x
⊢ IsPeriodicPt f n x
α : Type u_1
β : Type ?u.3348
f fa : α → α
fb : β → β
x y : α
m n : ℕ
g : α → α
hco : Commute f g
hfg : IsPeriodicPt (f ∘ g) n x
hg : IsPeriodicPt g n x
⊢ IsPeriodicPt f n x
rw [IsPeriodicPt, hco.comp_iterate] at hfg
no goals
α : Type u_1
β : Type ?u.3348
f fa : α → α
fb : β → β
x y : α
m n : ℕ
g : α → α
hco : Commute f g
hfg : IsFixedPt (f^[n] ∘ g^[n]) x
hg : IsPeriodicPt g n x
⊢ IsPeriodicPt f n x
exact hfg.left_of_comp hg