f g : CircleDeg1Lift
x : ℝ
n : ℕ
m : ℤ
h : ↑(f ^ n) x = x + ↑m
hn : 0 < n
this : τ (f ^ n) = ↑m
⊢ τ f = ↑m / ↑n
f g : CircleDeg1Lift
x : ℝ
n : ℕ
m : ℤ
h : ↑(f ^ n) x = x + ↑m
hn : 0 < n
⊢ τ f = ↑m / ↑n
have := (f ^ n).translationNumber_of_eq_add_int h
f g : CircleDeg1Lift
x : ℝ
n : ℕ
m : ℤ
h : ↑(f ^ n) x = x + ↑m
hn : 0 < n
this : τ f * ↑n = ↑m
⊢ ↑n ≠ 0
f g : CircleDeg1Lift
x : ℝ
n : ℕ
m : ℤ
h : ↑(f ^ n) x = x + ↑m
hn : 0 < n
this : τ (f ^ n) = ↑m
⊢ τ f = ↑m / ↑n
rwa [translationNumber_pow, mul_comm, ← eq_div_iff] at this
no goals
f g : CircleDeg1Lift
x : ℝ
n : ℕ
m : ℤ
h : ↑(f ^ n) x = x + ↑m
hn : 0 < n
this : τ f * ↑n = ↑m
⊢ ↑n ≠ 0
exact Nat.cast_ne_zero.2 (ne_of_gt hn)