conductorSet — Mathlib

English

The conductorSet χ is the set of natural numbers d such that χ factors through a character of level d.

Русский

ConductorSet χ — это множество натуральных чисел d, через которые χ факторизуется как символ уровня d.

LaTeX

$$$\operatorname{conductorSet}(\\chi) = \{ d \in \mathbb{N} \\mid \\operatorname{FactorsThrough}(\\chi,d) \}$$$

Lean4

/-- The set of natural numbers `d` such that `χ` factors through a character of level `d`. -/
def conductorSet : Set ℕ :=
  {d : ℕ | FactorsThrough χ d}

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