IsPrimitive — Mathlib

English

An additive character ψ is primitive if for every nonzero a, the multiplicative shift by a is not the trivial character.

Русский

Аддитивная характеристика ψ примитивна, если для каждого ненулевого a умножение (сдвиг по a) не даёт тривиальную характеристику.

LaTeX

$$IsPrimitive(ψ) iff ∀ a ≠ 0, mulShift ψ a ≠ 1$$

Lean4

/-- An additive character is *primitive* iff all its multiplicative shifts by nonzero
elements are nontrivial. -/
def IsPrimitive (ψ : AddChar R R') : Prop :=
  ∀ ⦃a : R⦄, a ≠ 0 → mulShift ψ a ≠ 1

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