toUnitHom_eq_char' — Mathlib

English

For a Dirichlet character χ and a unit a in ZMod n, χ(a) equals the value of the associated unit-hom χ.toUnitHom at a.

Русский

Для символа Дирихле χ и единицы a в ZMod n выполняется: χ(a) равно значению связанного гомоморфа по единицам χ.toUnitHom, применённому к a.

LaTeX

$$$$\\forall a \\in (\\mathbb{Z}/n\\mathbb{Z})^{\\times},\\quad χ(a) = (χ^{\\mathrm{toUnitHom}})(a).$$$$

Lean4

theorem toUnitHom_eq_char' {a : ZMod n} (ha : IsUnit a) : χ a = χ.toUnitHom ha.unit := by simp

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