isPrimitive_stdAddChar — Mathlib

English

The standard additive character is primitive.

Русский

Стандартный аддитивный характер примитивен.

LaTeX

$$IsPrimitive(\\mathrm{stdAddChar} (N))$$

Lean4

/-- The standard additive character `ZMod N → ℂ` is primitive. -/
theorem isPrimitive_stdAddChar (N : ℕ) [NeZero N] : (stdAddChar (N := N)).IsPrimitive :=
  by
  refine AddChar.zmod_char_primitive_of_eq_one_only_at_zero _ _ (fun t ht ↦ ?_)
  rwa [← (stdAddChar (N := N)).map_zero_eq_one, injective_stdAddChar.eq_iff] at ht

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