zmodChar_primitive_of_primitive_root

English

If ζ is a primitive n-th root of unity, then the additive character zmodChar n h((IsPrimitiveRoot.iff_def ζ n).mp h).left is primitive.

Русский

Если ζ — примитивный корень n-й степени единицы, то соответствующая аддитивная характеристика zmodChar является примитивной.

LaTeX

$$IsPrimitive( zmodChar n ((IsPrimitiveRoot.iff_def ζ n).mp h).left )$$

Lean4

/-- The additive character on `ZMod n` associated to a primitive `n`th root of unity
is primitive -/
theorem zmodChar_primitive_of_primitive_root (n : ℕ) [NeZero n] {ζ : C} (h : IsPrimitiveRoot ζ n) :
    IsPrimitive (zmodChar n ((IsPrimitiveRoot.iff_def ζ n).mp h).left) :=
  by
  apply zmod_char_primitive_of_eq_one_only_at_zero
  intro a ha
  rw [zmodChar_apply, ← pow_zero ζ] at ha
  exact (ZMod.val_eq_zero a).mp (IsPrimitiveRoot.pow_inj h (ZMod.val_lt a) (NeZero.pos _) ha)

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