f g : CircleDeg1Lift
hf : Continuous ↑f
m : ℤ
n : ℕ
hn : 0 < n
⊢ τ (f ^ n) = ↑m ↔ ∃ x, ↑(f ^ n) x = x + ↑m
f g : CircleDeg1Lift
hf : Continuous ↑f
m : ℤ
n : ℕ
hn : 0 < n
⊢ τ f = ↑m / ↑n ↔ ∃ x, ↑(f ^ n) x = x + ↑m
rw [eq_div_iff, mul_comm, ← translationNumber_pow] <;> [skip; exact ne_of_gt (Nat.cast_pos.2 hn)]
no goals
f g : CircleDeg1Lift
hf : Continuous ↑f
m : ℤ
n : ℕ
hn : 0 < n
⊢ τ (f ^ n) = ↑m ↔ ∃ x, ↑(f ^ n) x = x + ↑m
exact (f ^ n).translationNumber_eq_int_iff (f.continuous_pow hf n)