Bitwise
📁 Source: Batteries/Data/Nat/Bitwise.lean
Statistics
Nat
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
and_left_comm 📖 | — | — | — | — | — |
and_or_left_inj 📖 | — | — | — | — | and_or_left_injective |
and_or_left_injective 📖 | — | — | — | — | — |
and_or_right_inj 📖 | — | — | — | — | and_or_right_injective |
and_or_right_injective 📖 | — | — | — | — | — |
and_right_comm 📖 | — | — | — | — | — |
and_self_left 📖 | — | — | — | — | — |
and_self_right 📖 | — | — | — | — | — |
eq_of_xor_eq_zero 📖 | — | — | — | — | xor_xor_cancel_left |
or_left_comm 📖 | — | — | — | — | — |
or_right_comm 📖 | — | — | — | — | — |
or_self_left 📖 | — | — | — | — | — |
or_self_right 📖 | — | — | — | — | — |
xor_eq_zero_iff 📖 | — | — | — | — | eq_of_xor_eq_zero |
xor_left_comm 📖 | — | — | — | — | — |
xor_left_inj 📖 | — | — | — | — | xor_left_injective |
xor_left_injective 📖 | — | — | — | — | xor_xor_cancel_right |
xor_ne_zero_iff 📖 | — | — | — | — | — |
xor_right_comm 📖 | — | — | — | — | — |
xor_right_inj 📖 | — | — | — | — | xor_right_injective |
xor_right_injective 📖 | — | — | — | — | xor_xor_cancel_left |
xor_xor_cancel_left 📖 | — | — | — | — | — |
xor_xor_cancel_right 📖 | — | — | — | — | — |
---