shiftl_eq_shiftLeft — Mathlib

English

For every number p and natural n, the left-shift defined on Num coincides with the standard left-notation, i.e., p.shiftl n = p <<< n.

Русский

Для всякого числа p и натурального n левый сдвиг, определённый для Num, совпадает с обычной нотацией левого сдвига: p.shiftl n = p <<< n.

LaTeX

$$$p.shiftl n = p <<< n$$$

Lean4

@[simp]
theorem shiftl_eq_shiftLeft (p : Num) (n : Nat) : p.shiftl n = p <<< n :=
  rfl

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