mk_of_lt — Mathlib

English

If 0 < k, ζ^k = 1, and for every l with 0 < l < k we have ζ^l ≠ 1, then ζ is a primitive root of order k.

Русский

Если 0 < k, ζ^k = 1, и для всех l с 0 < l < k выполняется ζ^l ≠ 1, тогда ζ является примитивным корнем порядка k.

LaTeX

$$$0 < k \land ζ^k = 1 \land (\forall l:\mathbb{N}, 0 < l \land l < k \rightarrow ζ^l \neq 1) \Rightarrow IsPrimitiveRoot(ζ,k)$$$

Lean4

theorem mk_of_lt (ζ : M) (hk : 0 < k) (h1 : ζ ^ k = 1) (h : ∀ l : ℕ, 0 < l → l < k → ζ ^ l ≠ 1) : IsPrimitiveRoot ζ k :=
  by
  refine ⟨h1, fun l hl ↦ ?_⟩
  suffices k.gcd l = k by exact this ▸ k.gcd_dvd_right l
  rw [eq_iff_le_not_lt]
  refine ⟨Nat.le_of_dvd hk (k.gcd_dvd_left l), ?_⟩
  intro h'; apply h _ (Nat.gcd_pos_of_pos_left _ hk) h'
  exact pow_gcd_eq_one _ h1 hl

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