iff — Mathlib

English

For a fixed k>0, IsPrimitiveRoot ζ k is equivalent to ζ^k = 1 and ζ^l ≠ 1 for all 0 < l < k.

Русский

Для фиксированного k>0 изоморфизм: IsPrimitiveRoot ζ k эквивалентно ζ^k = 1 и ζ^l ≠ 1 для всех 0 < l < k.

LaTeX

$$$$\text{If } k>0,\ IsPrimitiveRoot(\zeta,k) \iff (\zeta^k = 1) \land (\forall l, 0

Lean4

protected theorem iff (hk : 0 < k) : IsPrimitiveRoot ζ k ↔ ζ ^ k = 1 ∧ ∀ l : ℕ, 0 < l → l < k → ζ ^ l ≠ 1 :=
  by
  refine ⟨fun h ↦ ⟨h.pow_eq_one, fun l hl' hl ↦ ?_⟩, fun ⟨hζ, hl⟩ ↦ IsPrimitiveRoot.mk_of_lt ζ hk hζ hl⟩
  rw [h.eq_orderOf] at hl
  exact pow_ne_one_of_lt_orderOf hl'.ne' hl

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