shiftLeft_sub — Mathlib

English

For any Nat m and {n k} with k ≤ n: m <<< (n − k) = (m <<< n) >>> k.

Русский

Для любого m и любых n,k с k ≤ n: m <<< (n−k) = (m <<< n) >>> k.

LaTeX

$$$$ \forall (m : \mathbb{N}) {n k : \mathbb{N}},\; k \le n \Rightarrow m \\<\\<\\< (n-k) = (m \\<< n) \\>> k. $$$$

Lean4

theorem shiftLeft_sub : ∀ (m : Nat) {n k}, k ≤ n → m <<< (n - k) = (m <<< n) >>> k := fun _ _ _ hk => by
  simp only [← shiftLeft'_false, shiftLeft'_sub false _ hk]

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