eq_changeLevel — Mathlib

English

There exists a unique Dirichlet character χ₀ of level d such that χ = changeLevel d χ₀.

Русский

Существует уникальный χ₀ уровня d, такой что χ = changeLevel d χ₀.

LaTeX

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

Lean4

/-- The fact that `χ` factors through `χ₀` of level `d` -/
theorem eq_changeLevel {d : ℕ} (h : FactorsThrough χ d) : χ = changeLevel h.dvd h.χ₀ :=
  Classical.choose_spec h.2

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