exists_gcd_eq_one_of_isOfFinAddOrder

English

Alternate formulation of the previous equivalence, relating addOrderOf(u) to the existence of m with m < n and gcd(m,n) = 1 and an explicit representative.

Русский

Альтернативная формулировка предыдущего эквивалентности: orderOf(u) равен n тогда и только тогда существует m < n и gcd(m,n)=1 и явно задаётся представитель.

LaTeX

$$addOrderOf(u) = n iff ∃ m < n, gcd(m,n) = 1 ∧ mk mp = u$$

Lean4

theorem exists_gcd_eq_one_of_isOfFinAddOrder {u : AddCircle p} (h : IsOfFinAddOrder u) :
    ∃ m : ℕ, m.gcd (addOrderOf u) = 1 ∧ m < addOrderOf u ∧ ↑((m : 𝕜) / addOrderOf u * p) = u :=
  let ⟨m, hl, hg, he⟩ := (addOrderOf_eq_pos_iff h.addOrderOf_pos).1 rfl
  ⟨m, hg, hl, he⟩

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