Theorems · Definition · number theory
Int.ldiff
ℤ → ℤ → ℤ
ldiff a b performs bitwise set difference. For each corresponding
pair of bits taken as Booleans, say aᵢ and bᵢ, it applies the
Boolean operation aᵢ ∧ ¬bᵢ to obtain the iᵗʰ bit of the result.
- Defined in
- Mathlib.Data.Int.Bitwise
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 29 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Nat.ldiffproof · cited by 4
Cited by3
Results whose statement or proof uses this declaration.
- Int.bitwise_diffstatement · cited by 2
- Int.ldiff_bitstatement · cited by 0
- Int.testBit_ldiffstatement · cited by 0