bit_mod_two

Mathlib.Data.Nat.BinaryRec

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

English

Let b ∈ {true,false}, n ∈ ℕ. Then bit b n mod 2 equals toNat(b) (0 or 1).

Русский

Пусть b ∈ {true,false}, n ∈ ℕ. Тогда bit b n mod 2 равно toNat(b) (0 или 1).

LaTeX

$$$ bit(b,n) \bmod 2 = \begin{cases}0,& b=\text{false} \\ 1,& b=\text{true} \end{cases}$$$

Lean4

@[simp]
theorem bit_mod_two (b n) : bit b n % 2 = b.toNat := by cases b <;> simp [bit_val]

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

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

Разделы

Аффилиация

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