DirichletCharacter — Mathlib

English

Dirichlet characters of level n with values in R are monoid homomorphisms from ZMod n to R.

Русский

Символы Дирихле модуля n (значения в R) являются гомоморфизмами моноида из ZMod n в R.

LaTeX

$$$\\operatorname{DirichletCharacter}(R,n) = \\operatorname{MulChar}(\\mathbb{Z}/n\\mathbb{Z}, R)$$$

Lean4

/-- The type of Dirichlet characters of level `n`. -/
abbrev DirichletCharacter (R : Type*) [CommMonoidWithZero R] (n : ℕ) :=
  MulChar (ZMod n) R

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