bit_ne_zero_iff

Mathlib.Data.Nat.Bitwise

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

English

For any n and b, n.bit b ≠ 0 iff (n = 0 → b = true).

Русский

Для любых n и b: n.bit b ≠ 0 тогда и только тогда, когда n = 0 → b = true.

LaTeX

$$$$ n\\text{.bit } b \\neq 0 \\quad\\iff\\quad (n = 0 \\to b = \\text{true}) $$$$

Lean4

theorem bit_ne_zero_iff {n : ℕ} {b : Bool} : n.bit b ≠ 0 ↔ n = 0 → b = true := by simp

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

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

Разделы

Аффилиация

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