isPrimitiveRoot_of_mem_rootsOfUnity

English

If a unit u belongs to rootsOfUnity n M, then there exists d>0 with d|n such that IsPrimitiveRoot u d.

Русский

Если u ∈ rootsOfUnity n M и u является единицей, то существует d>0, d|n, и IsPrimitiveRoot u d.

LaTeX

$$$$\exists d>0\ (d \mid n)\ \wedge\ IsPrimitiveRoot(u,d).$$$$

Lean4

theorem _root_.isPrimitiveRoot_of_mem_rootsOfUnity {u : Mˣ} {n : ℕ} [NeZero n] (hu : u ∈ rootsOfUnity n M) :
    ∃ d : ℕ, d ≠ 0 ∧ d ∣ n ∧ IsPrimitiveRoot u d :=
  ⟨orderOf u, (IsOfFinOrder.orderOf_pos ⟨n, NeZero.pos n, (isPeriodicPt_mul_iff_pow_eq_one u).mpr hu⟩).ne',
    orderOf_dvd_of_pow_eq_one hu, IsPrimitiveRoot.orderOf u⟩

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