zmodChar — Mathlib

English

Definition: zmodChar(n,hζ) defines an additive character on ZMod n by mapping a to ζ^{a.val} when ζ^n = 1.

Русский

Определение: zmodChar(n,hζ) задаёт аддитивную характеристику на ZMod n по правилу a ↦ ζ^{a.val}, если ζ^n = 1.

LaTeX

$$zmodChar(n,hζ): ZMod n → C, a ↦ ζ^{a.val}, with ζ^n = 1$$

Lean4

/-- We can define an additive character on `ZMod n` when we have an `n`th root of unity `ζ : C`. -/
def zmodChar (n : ℕ) [NeZero n] {ζ : C} (hζ : ζ ^ n = 1) : AddChar (ZMod n) C
    where
  toFun a := ζ ^ a.val
  map_zero_eq_one' := by simp only [ZMod.val_zero, pow_zero]
  map_add_eq_mul' x y := by simp only [ZMod.val_add, ← pow_eq_pow_mod _ hζ, ← pow_add]

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