p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
n : ℕ := addOrderOf u
⊢ ∃ k, ‖u‖ = p * (↑k / ↑(addOrderOf u))
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
⊢ ∃ k, ‖u‖ = p * (↑k / ↑(addOrderOf u))
let n := addOrderOf u
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
n : ℕ := addOrderOf u
⊢ ∃ k, ‖u‖ = p * (↑k / ↑n)
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
n : ℕ := addOrderOf u
⊢ ∃ k, ‖u‖ = p * (↑k / ↑(addOrderOf u))
change ∃ k : ℕ, ‖u‖ = p * (k / n)
case intro.intro.intro
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
n : ℕ := addOrderOf u
m : ℕ
hm : ↑(↑m / ↑(addOrderOf u) * p) = u
⊢ ∃ k, ‖u‖ = p * (↑k / ↑n)
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
n : ℕ := addOrderOf u
⊢ ∃ k, ‖u‖ = p * (↑k / ↑n)
obtain ⟨m, -, -, hm⟩ := exists_gcd_eq_one_of_isOfFinAddOrder hu
case intro.intro.intro
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
n : ℕ := addOrderOf u
m : ℕ
hm : ↑(↑m / ↑(addOrderOf u) * p) = u
⊢ ‖u‖ = p * (↑(min (m % n) (n - m % n)) / ↑n)
case intro.intro.intro
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
n : ℕ := addOrderOf u
m : ℕ
hm : ↑(↑m / ↑(addOrderOf u) * p) = u
⊢ ∃ k, ‖u‖ = p * (↑k / ↑n)
refine' ⟨min (m % n) (n - m % n), _⟩
no goals
case intro.intro.intro
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu : IsOfFinAddOrder u
n : ℕ := addOrderOf u
m : ℕ
hm : ↑(↑m / ↑(addOrderOf u) * p) = u
⊢ ‖u‖ = p * (↑(min (m % n) (n - m % n)) / ↑n)
rw [← hm, norm_div_nat_cast]