conductor

Mathlib.NumberTheory.DirichletCharacter.Basic

URI: https://scilib.ai/kg/mathlib#DirichletCharacter.conductor

English

The conductor χ is the least natural number through which χ factors.

Русский

Кондуктор χ — наименьшее натуральное число, через которое χ факторизуется.

LaTeX

$$$\operatorname{conductor}(\\chi) = \min(\\operatorname{conductorSet}(\\chi))$$$

Lean4

/-- The minimum natural number level `n` through which `χ` factors. -/
noncomputable def conductor : ℕ :=
  sInf (conductorSet χ)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru