𝕜 : Type u_1
B : Type ?u.192515
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q✝ : 𝕜
hp : Fact (0 < p)
q : ℚ
this : ↑↑q.den ≠ 0
⊢ addOrderOf ↑(↑q * p) = q.den
𝕜 : Type u_1
B : Type ?u.192515
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q✝ : 𝕜
hp : Fact (0 < p)
q : ℚ
⊢ addOrderOf ↑(↑q * p) = q.den
have : (↑(q.den : ℤ) : 𝕜) ≠ 0 := by
  norm_cast
  exact q.pos.ne.symm
no goals
𝕜 : Type u_1
B : Type ?u.192515
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q✝ : 𝕜
hp : Fact (0 < p)
q : ℚ
this : ↑↑q.den ≠ 0
⊢ addOrderOf ↑(↑q * p) = q.den
rw [← @Rat.num_den q, Rat.cast_mk_of_ne_zero _ _ this, Int.cast_ofNat, Rat.num_den,
  addOrderOf_div_of_gcd_eq_one' q.pos q.reduced]
𝕜 : Type u_1
B : Type ?u.192515
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q✝ : 𝕜
hp : Fact (0 < p)
q : ℚ
⊢ ¬q.den = 0
𝕜 : Type u_1
B : Type ?u.192515
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q✝ : 𝕜
hp : Fact (0 < p)
q : ℚ
⊢ ↑↑q.den ≠ 0
norm_cast
no goals
𝕜 : Type u_1
B : Type ?u.192515
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q✝ : 𝕜
hp : Fact (0 < p)
q : ℚ
⊢ ¬q.den = 0
exact q.pos.ne.symm