dvd — Mathlib

English

If χ factors through level d, there exists a unique χ′ at level d such that χ = changeLevel d χ′.

Русский

Если χ факторизуется через уровень d, существует единственный χ′ на уровне d такой, что χ = changeLevel d χ′.

LaTeX

$$$$ \\exists! χ' : \\operatorname{DirichletCharacter}(R,d),\\; χ = \\operatorname{changeLevel}_{n\\to d}(χ'). $$$$

Lean4

/-- The fact that `d` divides `n` when `χ` factors through a Dirichlet character at level `d` -/
theorem dvd {d : ℕ} (h : FactorsThrough χ d) : d ∣ n :=
  h.1

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