exists_norm_eq_of_isOfFinAddOrder

English

If u has finite additive order in AddCircle(p), then there exists k ∈ ℕ such that ‖u‖ = p · (k / addOrderOf u).

Русский

Если у имеет конечную порядковость по сложению в AddCircle(p), то существует k ∈ ℕ такое, что ‖u‖ = p · (k / addOrderOf(u)).

LaTeX

$$$\\exists k \\in \\mathbb{N}, \\; \\|u\\| = p \\cdot \\left( \\dfrac{k}{\\operatorname{addOrderOf} u} \\right)$$$

Lean4

theorem exists_norm_eq_of_isOfFinAddOrder {u : AddCircle p} (hu : IsOfFinAddOrder u) :
    ∃ k : ℕ, ‖u‖ = p * (k / addOrderOf u) := by
  let n := addOrderOf u
  change ∃ k : ℕ, ‖u‖ = p * (k / n)
  obtain ⟨m, -, -, hm⟩ := exists_gcd_eq_one_of_isOfFinAddOrder hu
  refine ⟨min (m % n) (n - m % n), ?_⟩
  rw [← hm, norm_div_natCast]

Похожие утверждения