bitwise_zero_left — Mathlib

English

If the left operand is zero, then bitwise f 0 m is either m or 0, depending on f(false, true): bitwise f 0 m = if f(false, true) then m else 0.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem bitwise_zero_left (m : Nat) : bitwise f 0 m = if f false true then m else 0 := by simp [bitwise]

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