HepLean Documentation
Init
.
Data
.
Fin
.
Bitwise
Search
Google site search
return to top
source
Imports
Init.Data.Fin.Basic
Init.Data.Nat.Bitwise
Imported by
Fin
.
and_val
source
@[simp]
theorem
Fin
.
and_val
{n :
Nat
}
(a b :
Fin
n
)
:
↑
(
a
&&&
b
)
=
↑
a
&&&
↑
b