𝕜 : Type u_1
B : Type ?u.183351
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n m : ℕ
hn : 0 < n
⊢ Nat.gcd m n * (addOrderOf ↑(p / ↑n) / Nat.gcd (addOrderOf ↑(p / ↑n)) m) = n

case h
𝕜 : Type u_1
B : Type ?u.183351
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n m : ℕ
hn : 0 < n
⊢ IsOfFinAddOrder ↑(p / ↑n)
𝕜 : Type u_1
B : Type ?u.183351
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n m : ℕ
hn : 0 < n
⊢ Nat.gcd m n * addOrderOf ↑(↑m / ↑n * p) = n
rw [mul_comm_div, ← nsmul_eq_mul, coe_nsmul, addOrderOf_nsmul'']
𝕜 : Type u_1
B : Type ?u.183351
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n m : ℕ
hn : 0 < n
⊢ Nat.gcd n m ∣ n
𝕜 : Type u_1
B : Type ?u.183351
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n m : ℕ
hn : 0 < n
⊢ Nat.gcd m n * (addOrderOf ↑(p / ↑n) / Nat.gcd (addOrderOf ↑(p / ↑n)) m) = n
rw [addOrderOf_period_div hn, Nat.gcd_comm, Nat.mul_div_cancel']
no goals
𝕜 : Type u_1
B : Type ?u.183351
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n m : ℕ
hn : 0 < n
⊢ Nat.gcd n m ∣ n
exact n.gcd_dvd_left m
case h
𝕜 : Type u_1
B : Type ?u.183351
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n m : ℕ
hn : 0 < n
⊢ 0 < n
case h
𝕜 : Type u_1
B : Type ?u.183351
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n m : ℕ
hn : 0 < n
⊢ IsOfFinAddOrder ↑(p / ↑n)
rw [← addOrderOf_pos_iff, addOrderOf_period_div hn]
no goals
case h
𝕜 : Type u_1
B : Type ?u.183351
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
n m : ℕ
hn : 0 < n
⊢ 0 < n
exact hn