exists_pos — Mathlib

English

If ζ^k = 1 with k ≠ 0, there exists k' > 0 such that IsPrimitiveRoot ζ k'.

Русский

Если ζ^k = 1 и k ≠ 0, существует k' > 0 такое, что IsPrimitiveRoot ζ k'.

LaTeX

$$$$\exists k'>0, IsPrimitiveRoot(\zeta,k').$$$$

Lean4

theorem exists_pos {k : ℕ} (hζ : ζ ^ k = 1) (hk : k ≠ 0) : ∃ k' > 0, IsPrimitiveRoot ζ k' :=
  ⟨orderOf ζ, by
    rw [gt_iff_lt, orderOf_pos_iff, isOfFinOrder_iff_pow_eq_one]
    exact ⟨k, Nat.pos_iff_ne_zero.mpr hk, hζ⟩, .orderOf _⟩

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