Theorems · Inductive type
LawfulXor
(α : Type u_1) → [XorOp α] → [Zero α] → Prop
A typeclass indicating that the xor operation, ^^^, is lawful.
- Defined in
- Mathlib.Data.LawfulXor.Basic
- Cited by
- 28 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by31
Results whose statement or proof uses this declaration.
- Equiv.xorstatement and proof · cited by 7
- zero_xorstatement and proof · cited by 4
- LawfulXor.xor_commstatement and proof · cited by 4
- LawfulXor.xor_selfstatement and proof · cited by 4
- LawfulXor.xor_assocstatement and proof · cited by 3
- LawfulXor.xor_zerostatement and proof · cited by 3
- xor_cancel_rightstatement and proof · cited by 3
- xor_eq_iff_left_eqstatement and proof · cited by 2
- xor_left_eq_id_iffstatement and proof · cited by 2
- xor_right_eqstatement and proof · cited by 2
- xor_right_involutivestatement and proof · cited by 2
- isFixedPt_xor_left_iffstatement and proof · cited by 2