eval_neg

Mathlib.NumberTheory.DirichletCharacter.Basic

URI: https://scilib.ai/kg/mathlib#DirichletCharacter.Odd.eval_neg

English

In DirichletCharacter.Odd, even implies not odd; i.e., Even(χ) ⇒ ¬ Odd(χ).

Русский

В DirichletCharacter.Odd чётность приводит к ненечетности; т.е. Even(χ) ⇒ ¬ Odd(χ).

LaTeX

$$$\\text{Odd.not\\_odd}: \\forall ψ\\,(\\text{Even}(ψ) \\Rightarrow \\neg \\text{Odd}(ψ)).$$$

Lean4

theorem eval_neg (x : ZMod m) (hψ : ψ.Odd) : ψ (-x) = -ψ x :=
  by
  rw [Odd] at hψ
  rw [← neg_one_mul, map_mul]
  simp [hψ]

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

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

Разделы

Аффилиация

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