not_even_and_odd — Mathlib

English

No Dirichlet character ψ can be both even and odd (assuming NeZero 2).

Русский

Ни один символ Дирихле не может быть одновременно четным и нечетным (при условии NeZero 2).

LaTeX

$$$\\neg(\\psi.Even \\wedge \\psi.Odd).$$$

Lean4

theorem not_even_and_odd [NeZero (2 : S)] : ¬(ψ.Even ∧ ψ.Odd) :=
  by
  rintro ⟨(h : _ = 1), (h' : _ = -1)⟩
  simp only [h', neg_eq_iff_add_eq_zero, one_add_one_eq_two, two_ne_zero] at h

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