bit_mod_two_eq_zero_iff

Mathlib.Data.Nat.Bitwise

URI: https://scilib.ai/kg/mathlib#Nat.bit_mod_two_eq_zero_iff

English

For any a ∈ {true,false} and x ∈ ℕ, bit a x ≡ 0 (mod 2) if and only if a is false.

Русский

Для любых a ∈ {true,false} и x ∈ ℕ: бит a x чётен тогда и только тогда, когда a = false.

LaTeX

$$$$ bit\\ a\\ x\\ %\\ 2 = 0 \\iff \\lnot a $$$$

Lean4

theorem bit_mod_two_eq_zero_iff (a x) : bit a x % 2 = 0 ↔ !a := by simp

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

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

Разделы

Аффилиация

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