case h.e'_2
𝕜 : Type u_1
B : Type ?u.185954
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
m n : ℕ
hn : 0 < n
h : Nat.gcd m n = 1
⊢ addOrderOf ↑(↑m / ↑n * p) = Nat.gcd m n * addOrderOf ↑(↑m / ↑n * p)
𝕜 : Type u_1
B : Type ?u.185954
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
m n : ℕ
hn : 0 < n
h : Nat.gcd m n = 1
⊢ addOrderOf ↑(↑m / ↑n * p) = n
convert gcd_mul_addOrderOf_div_eq p m hn
no goals
case h.e'_2
𝕜 : Type u_1
B : Type ?u.185954
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p q : 𝕜
hp : Fact (0 < p)
m n : ℕ
hn : 0 < n
h : Nat.gcd m n = 1
⊢ addOrderOf ↑(↑m / ↑n * p) = Nat.gcd m n * addOrderOf ↑(↑m / ↑n * p)
rw [h, one_mul]