eval_modulus_sub

Mathlib.NumberTheory.DirichletCharacter.Basic

URI: https://scilib.ai/kg/mathlib#DirichletCharacter.eval_modulus_sub

English

For χ and x in ZMod n, χ(n − x) = χ(−x).

Русский

Для χ и x в ZMod n выполняется χ(n − x) = χ(−x).

LaTeX

$$$$\\forall x \\in \\mathbb{Z}/n\\mathbb{Z},\\quad χ(n - x) = χ(-x).$$$$

Lean4

theorem eval_modulus_sub (x : ZMod n) : χ (n - x) = χ (-x) := by simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru