primitiveZModChar — Mathlib

English

There exists a primitive additive character on ZMod n when the characteristic of the target does not divide n.

Русский

Существует примитивная аддитивная характеристика на ZMod n, если характеристика целевой кольца не делит n.

LaTeX

$$There exists AddChar.PrimitiveAddChar on ZMod n under ringChar F' not dividing n$$

Lean4

/-- There is a primitive additive character on `ZMod n` if the characteristic of the target
does not divide `n` -/
noncomputable def primitiveZModChar (n : ℕ+) (F' : Type v) [Field F'] (h : (n : F') ≠ 0) :
    PrimitiveAddChar (ZMod n) F' :=
  have : NeZero (n : F') := ⟨h⟩
  ⟨n, zmodChar n (IsCyclotomicExtension.zeta_pow n F' _),
    zmodChar_primitive_of_primitive_root n (IsCyclotomicExtension.zeta_spec n F' _)⟩

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