not_odd

Mathlib.NumberTheory.DirichletCharacter.Basic

URI: https://scilib.ai/kg/mathlib#DirichletCharacter.Even.not_odd

English

If ψ is even, then ψ is not odd; i.e., Even(ψ) implies Not Odd(ψ).

Русский

Если ψ чётный, то ψ не нечетный; т.е. Even(ψ) ⇒ ¬Odd(ψ).

LaTeX

$$$\\text{Even.not_odd}: \\text{Even}(\\psi) \\implies \\neg \\text{Odd}(\\psi).$$$

Lean4

theorem not_odd [NeZero (2 : S)] (hψ : Even ψ) : ¬Odd ψ :=
  not_and.mp ψ.not_even_and_odd hψ

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

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

Разделы

Аффилиация

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