Lemmas about size
.
shiftl
and shiftr
#
size
#
@[simp]
theorem
Nat.size_shiftl'
{b : Bool}
{m : ℕ}
{n : ℕ}
(h : Nat.shiftl' b m n ≠ 0)
:
Nat.size (Nat.shiftl' b m n) = Nat.size m + n
Mathlib.Data.Nat.Size
Lemmas about size
.
shiftl
and shiftr
#size
#