odd_iff_imp

Mathlib.Data.Fin.Parity

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

English

Odd k is equivalent to the condition that if n is even then k.val is odd.

Русский

Нечетность k эквивалентна условию: если n четно, то k.val нечетно.

LaTeX

$$$\mathrm{Odd}(k) \iff [\mathrm{Even}(n) \rightarrow \mathrm{Odd}(k.\mathrm{val})].$$$

Lean4

theorem odd_iff_imp [NeZero n] : Odd k ↔ (Even n → Odd k.val) :=
  by
  rw [imp_iff_not_or, Nat.not_even_iff_odd]
  exact odd_iff

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

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

Разделы

Аффилиация

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