HepLean Documentation
Init
.
Data
.
Int
.
Bitwise
.
Lemmas
Search
Google site search
return to top
source
Imports
Init.Data.Int.Bitwise
Init.Data.Nat.Bitwise.Lemmas
Imported by
Int
.
shiftRight_eq
Int
.
natCast_shiftRight
Int
.
negSucc_shiftRight
Int
.
shiftRight_add
Int
.
shiftRight_eq_div_pow
Int
.
zero_shiftRight
source
theorem
Int
.
shiftRight_eq
(n :
Int
)
(s :
Nat
)
:
n
>>>
s
=
n
.shiftRight
s
source
@[simp]
theorem
Int
.
natCast_shiftRight
(n s :
Nat
)
:
↑
n
>>>
s
=
↑
(
n
>>>
s
)
source
@[simp]
theorem
Int
.
negSucc_shiftRight
(m n :
Nat
)
:
Int.negSucc
m
>>>
n
=
Int.negSucc
(
m
>>>
n
)
source
theorem
Int
.
shiftRight_add
(i :
Int
)
(m n :
Nat
)
:
i
>>>
(
m
+
n
)
=
i
>>>
m
>>>
n
source
theorem
Int
.
shiftRight_eq_div_pow
(m :
Int
)
(n :
Nat
)
:
m
>>>
n
=
m
/
↑
(
2
^
n
)
source
@[simp]
theorem
Int
.
zero_shiftRight
(n :
Nat
)
:
0
>>>
n
=
0