def commandDeclare_bitwise_uint_theorems_ : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem UInt8.and_toNat (a : UInt8) (b : UInt8) : (a &&& b).toNat = a.toNat &&& b.toNat

@[simp]

theorem UInt16.and_toNat (a : UInt16) (b : UInt16) : (a &&& b).toNat = a.toNat &&& b.toNat

@[simp]

theorem UInt32.and_toNat (a : UInt32) (b : UInt32) : (a &&& b).toNat = a.toNat &&& b.toNat

@[simp]

theorem UInt64.and_toNat (a : UInt64) (b : UInt64) : (a &&& b).toNat = a.toNat &&& b.toNat

@[simp]

theorem USize.and_toNat (a : USize) (b : USize) : (a &&& b).toNat = a.toNat &&& b.toNat