zmod_char_ne_one_iff — Mathlib

English

A primitive additive character ψ on ZMod n is equivalent to ψ(1) ≠ 1; more precisely ψ ≠ 1 iff ψ(1) ≠ 1.

Русский

Аддитивная характеристика ψ на ZMod n примитивна тогда и только тогда, когда ψ(1) ≠ 1; точнее, ψ ≠ 1 ⇔ ψ(1) ≠ 1.

LaTeX

$$ψ ≠ 1 ⇔ ψ(1) ≠ 1$$

Lean4

/-- An additive character on `ZMod n` is nontrivial iff it takes a value `≠ 1` on `1`. -/
theorem zmod_char_ne_one_iff (n : ℕ) [NeZero n] (ψ : AddChar (ZMod n) C) : ψ ≠ 1 ↔ ψ 1 ≠ 1 :=
  by
  rw [ne_one_iff]
  refine ⟨?_, fun h => ⟨_, h⟩⟩
  contrapose!
  rintro h₁ a
  have ha₁ : a = a.val • (1 : ZMod ↑n) := by rw [nsmul_eq_mul, mul_one]; exact (ZMod.natCast_zmod_val a).symm
  rw [ha₁, map_nsmul_eq_pow, h₁, one_pow]

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