bitwise_zero_right — Mathlib

English

If the right operand is zero, then bitwise f n 0 equals n or 0 depending on f(true,false): bitwise f n 0 = if f(true,false) then n else 0.

Русский

Если правая часть равна нулю, то bitwise f n 0 равняется n или 0, в зависимости от f(true,false): bitwise f n 0 = if f(true,false) then n else 0.

LaTeX

$$$$ \\mathrm{bitwise}\\; f\\; n\\; 0 = \\begin{cases} n, & \\text{если } f(1,0) = \\text{true} \\\\ 0, & \\text{иначе} \\end{cases} $$$$

Lean4

@[simp]
theorem bitwise_zero_right (n : Nat) : bitwise f n 0 = if f true false then n else 0 :=
  by
  unfold bitwise
  simp only [ite_self, Nat.zero_div, ite_true, ite_eq_right_iff]
  rintro ⟨⟩
  split_ifs <;> rfl

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