primitiveCharacter — Mathlib

English

The primitiveCharacter of χ is a DirichletCharacter of modulus χ.conductor.

Русский

Примитивный символ χ имеет модуль χ.conductor.

LaTeX

$$$\operatorname{primitiveCharacter}(\\chi) : \mathrm{DirichletCharacter}(R, \\operatorname{conductor}(\\chi))$$$

Lean4

/-- The primitive character associated to a Dirichlet character. -/
noncomputable def primitiveCharacter : DirichletCharacter R χ.conductor :=
  Classical.choose (factorsThrough_conductor χ).choose_spec

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