changeLevel_one — Mathlib

English

For a Dirichlet character χ of modulus n and any d with d ∣ n, changing the level to d of the trivial character yields the trivial character.

Русский

Для χ символь Дирихле модуля n и любого d, делящего n, переход к уровню d тривиального символа даёт тривиальный символ.

LaTeX

$$$\\mathrm{changeLevel}(h)(1 : \\mathrm{DirichletCharacter}(R,d)) = 1$$$

Lean4

theorem changeLevel_one {d : ℕ} (h : d ∣ n) : changeLevel h (1 : DirichletCharacter R d) = 1 := by simp

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