zmod_char_primitive_of_eq_one_only_at_zero

English

Converse: if additive character takes value 1 only at 0, then it is primitive.

Русский

Обратно: если характеристика принимает значение 1 только при 0, то она примитивна.

LaTeX

$$∑$$

Lean4

/-- The converse: if the additive character takes the value `1` only at `0`,
then it is primitive. -/
theorem zmod_char_primitive_of_eq_one_only_at_zero (n : ℕ) (ψ : AddChar (ZMod n) C) (hψ : ∀ a, ψ a = 1 → a = 0) :
    IsPrimitive ψ := by
  refine fun a ha hf => ?_
  have h : mulShift ψ a 1 = (1 : AddChar (ZMod n) C) (1 : ZMod n) := congr_fun (congr_arg (↑) hf) 1
  rw [mulShift_apply, mul_one] at h; norm_cast at h
  exact ha (hψ a h)

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