bit_eq_zero_iff

Mathlib.Data.Nat.BinaryRec

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

← MathLib Explorer

English

bit b n equals 0 if and only if n = 0 and b = false.

Русский

bit b n = 0 тогда и только тогда, когда n = 0 и b = ложь.

LaTeX

$$$\text{bit}(b,n)=0 \iff (n=0) \land (b=\text{false})$$$

Lean4

@[simp]
theorem bit_eq_zero_iff {n : Nat} {b : Bool} : bit b n = 0 ↔ n = 0 ∧ b = false := by
  cases n <;> cases b <;> simp [bit, Nat.two_mul, ← Nat.add_assoc]

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

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

Разделы

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

Аффилиация

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