not_even

Mathlib.NumberTheory.DirichletCharacter.Basic

URI: https://scilib.ai/kg/mathlib#DirichletCharacter.Odd.not_even

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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