injOn_pow_mul — Mathlib

English

If h is a primitive root ζ n and α ≠ 0, then the map x ↦ ζ^x · α is injective on {0,...,n-1}.

Русский

Если h — примитивный корень ζ n и α ≠ 0, то отображение x ↦ ζ^x · α инъективно на {0,...,n-1}.

LaTeX

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

Lean4

theorem injOn_pow_mul {n : ℕ} {ζ : M₀} (hζ : IsPrimitiveRoot ζ n) {α : M₀} (hα : α ≠ 0) :
    Set.InjOn (ζ ^ · * α) (Finset.range n) := fun i hi j hj e ↦
  hζ.injOn_pow hi hj (by simpa [mul_eq_mul_right_iff, or_iff_left hα] using e)

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