zmod_char_eq_one_iff — Mathlib

English

If ψ(a) = 1 implies a = 0 for all a ∈ ZMod n, then ψ is primitive.

Русский

Если для всех a ∈ ZMod n равенство ψ(a) = 1 тогда и только тогда, когда a = 0, то ψ примитивна.

LaTeX

$$∀ a, ψ(a) = 1 → a = 0 ⇒ IsPrimitive(ψ)$$

Lean4

/-- A primitive additive character on `ZMod n` takes the value `1` only at `0`. -/
theorem zmod_char_eq_one_iff (n : ℕ) [NeZero n] {ψ : AddChar (ZMod n) C} (hψ : IsPrimitive ψ) (a : ZMod n) :
    ψ a = 1 ↔ a = 0 :=
  by
  refine ⟨fun h => not_imp_comm.mp (@hψ a) ?_, fun ha => by rw [ha, map_zero_eq_one]⟩
  rw [zmod_char_ne_one_iff n (mulShift ψ a), mulShift_apply, mul_one, h, Classical.not_not]

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