zero_of_even_and_odd — Mathlib

English

If a function is both even and odd, it is identically zero.

Русский

Если функция одновременно чётна и нечётна, она тождественно равна нулю.

LaTeX

$$$f = 0$$$

Lean4

/-- If `f` is both even and odd, and its target is a torsion-free commutative additive group,
then `f = 0`.
-/
theorem zero_of_even_and_odd [Neg α] (he : f.Even) (ho : f.Odd) : f = 0 :=
  by
  ext r
  rw [Pi.zero_apply, ← neg_eq_self ℕ, ← ho, he]

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