to_fun — Mathlib

English

If ψ is odd, then ψ as a function is odd: ψ(-x) = -ψ(x) for all x.

Русский

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

LaTeX

$$$\\text{Odd.to\\_fun}: \\text{If } ψ\\text{ is odd, then } ψ(-x)=-ψ(x) \\text{ for all } x.$$$

Lean4

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

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