shift2 — Mathlib

English

Given a,b ∈ ℕ, define a function φ: ℤ → ℕ × ℕ by φ(e) = (a · 2^e, b) if e ≥ 0, and φ(e) = (a, b · 2^{|e|}) if e < 0, i.e., using binary shifts.

Русский

Задать отображение φ: ℤ → ℕ × ℕ так, чтобы φ(e) = (a·2^e, b) при e ≥ 0 и φ(e) = (a, b·2^{|e|}) при e < 0.

LaTeX

$$$\\text{shift2}(a,b)(e) = \\begin{cases} (a \\cdot 2^{e}, b) & \\text{if } e \\ge 0, \\\\ (a, b \\cdot 2^{-e}) & \\text{if } e < 0. \\end{cases}$$$

Lean4

@[nolint docBlame]
def shift2 (a b : ℕ) : ℤ → ℕ × ℕ
  | Int.ofNat e => (a <<< e, b)
  | Int.negSucc e => (a, b <<< e.succ)

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