injOn_pow — Mathlib

English

If h is a primitive root of order n, then the map i ↦ ζ^i is injective on {0,...,n−1}.

Русский

Если ζ — примитивный корень порядка n, то отображение i ↦ ζ^i на множество {0,...,n−1} инъективно.

LaTeX

$$$$\text{If } IsPrimitiveRoot(\zeta,n), \text{ then } \{0,1,...,n-1\} \to \zeta^i \text{ is injective}. $$$$

Lean4

theorem injOn_pow {n : ℕ} {ζ : M} (hζ : IsPrimitiveRoot ζ n) : Set.InjOn (ζ ^ ·) (Finset.range n) :=
  by
  intro i hi j hj e
  rw [Finset.coe_range, Set.mem_Iio] at hi hj
  exact hζ.pow_inj hi hj e

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