modZero_eq_delta — Mathlib

English

The Dirichlet character modulo 0 corresponds to the delta function: the twist equals δ.

Русский

Dirichlet-символ модуля 0 соответствует δ; поворот χ· равен δ.

LaTeX

$$$(\text{mod } 0\text{ }χ) = \delta.$$$

Lean4

/-- The Dirichlet character mod `0` corresponds to `δ`. -/
theorem modZero_eq_delta {χ : DirichletCharacter ℂ 0} : ↗χ = δ :=
  by
  ext n
  rcases eq_or_ne n 0 with rfl | hn
  · simp_rw [cast_zero, χ.map_nonunit not_isUnit_zero, delta, reduceCtorEq, if_false]
  rcases eq_or_ne n 1 with rfl | hn'
  · simp [delta]
  have : ¬IsUnit (n : ZMod 0) := fun h ↦ hn' <| ZMod.eq_one_of_isUnit_natCast h
  simp_all [χ.map_nonunit this, delta]

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