to_fun — Mathlib

English

If χ is an even Dirichlet character, then χ, viewed as a function, is an even function: χ(-x) = χ(x) for all x.

Русский

Если χ — чётный символ Дирихле, то он как функция является чётной: χ(-x)=χ(x) для всех x.

LaTeX

$$$\\text{Even.to\\_fun}: \\text{If } \\text{Even}(χ), \\text{ then } χ \\text{ is a function-even; } χ(-x)=χ(x).$$$

Lean4

/-- An even Dirichlet character is an even function. -/
theorem to_fun {χ : DirichletCharacter S m} (hχ : Even χ) : Function.Even χ := fun _ ↦ by
  rw [← neg_one_mul, map_mul, hχ, one_mul]

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