not_even_iff_odd_of_even

Mathlib.Data.Fin.Parity

URI: https://scilib.ai/kg/mathlib#Fin.not_even_iff_odd_of_even

← MathLib Explorer

English

For even n, not even k is equivalent to odd k.

Русский

Для четного n нечетность k эквивалентна нечетности.

LaTeX

$$$\forall n:\mathbb{N},\; \mathrm{Even}(n) \rightarrow \lnot \mathrm{Even}(k) \iff \mathrm{Odd}(k).$$$

Lean4

theorem not_even_iff_odd_of_even [NeZero n] (hn : Even n) : ¬Even k ↔ Odd k :=
  by
  rw [even_iff_of_even hn, odd_iff_of_even hn]
  exact Nat.not_even_iff_odd

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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