Documentation

Mathlib.Data.LawfulXor.Basic

The LawfulXor typeclass #

This file generalizes basic lemmas about the ^^^ operator across numeric types.

source
class LawfulXor (α : Type u_1) [XorOp α] [Zero α] :
Prop

A typeclass indicating that the xor operation, ^^^, is lawful.

  • xor_assoc (a b c : α) : a ^^^ b ^^^ c = a ^^^ (b ^^^ c)
  • xor_self (a : α) : a ^^^ a = 0
  • xor_zero (a : α) : a ^^^ 0 = a
  • xor_comm (a b : α) : a ^^^ b = b ^^^ a
Instances
    source
    @[simp]
    theorem zero_xor {α : Type u_1} [XorOp α] [Zero α] [LawfulXor α] (a : α) :
    0 ^^^ a = a
    source
    instance instCommutativeXor_mathlib {α : Type u_1} [XorOp α] [Zero α] [LawfulXor α] :
    Std.Commutative XorOp.xor
    source
    instance instAssociativeXor_mathlib {α : Type u_1} [XorOp α] [Zero α] [LawfulXor α] :
    Std.Associative XorOp.xor
    source
    instance instLawfulCommIdentityXorOfNat_mathlib {α : Type u_1} [XorOp α] [Zero α] [LawfulXor α] :
    Std.LawfulCommIdentity XorOp.xor 0
    source
    @[simp]
    theorem xor_cancel_left {α : Type u_1} [XorOp α] [Zero α] [LawfulXor α] (a b : α) :
    a ^^^ (a ^^^ b) = b
    source
    @[simp]
    theorem xor_cancel_right {α : Type u_1} [XorOp α] [Zero α] [LawfulXor α] (a b : α) :
    a ^^^ b ^^^ b = a
    source
    instance instLawfulXorNat :
    LawfulXor ℕ
    source
    instance instLawfulXorFinHPowNatOfNat {w : ℕ} :
    LawfulXor (Fin (2 ^ w))
    source
    instance instLawfulXorBitVec {w : ℕ} :
    LawfulXor (BitVec w)
    source
    instance instLawfulXorUInt8 :
    LawfulXor UInt8
    source
    instance instLawfulXorUInt16 :
    LawfulXor UInt16
    source
    instance instLawfulXorUInt32 :
    LawfulXor UInt32
    source
    instance instLawfulXorUInt64 :
    LawfulXor UInt64
    source
    instance instLawfulXorUSize :
    LawfulXor USize
    source
    instance instLawfulXorInt8 :
    LawfulXor Int8
    source
    instance instLawfulXorInt16 :
    LawfulXor Int16
    source
    instance instLawfulXorInt32 :
    LawfulXor Int32
    source
    instance instLawfulXorInt64 :
    LawfulXor Int64
    source
    instance instLawfulXorISize :
    LawfulXor ISize
    source
    theorem xor_right_eq {α : Type u_1} [XorOp α] [Zero α] [LawfulXor α] {a : α} :
    (fun (x : α) => x ^^^ a) = fun (x : α) => a ^^^ x
    source
    theorem xor_left_involutive {α : Type u_1} [XorOp α] [Zero α] [LawfulXor α] (a : α) :
    Function.Involutive fun (x : α) => x ^^^ a
    source
    theorem xor_right_involutive {α : Type u_1} [XorOp α] [Zero α] [LawfulXor α] (a : α) :
    Function.Involutive fun (x : α) => a ^^^ x
    source
    theorem xor_eq_iff_left_eq {α : Type u_1} [XorOp α] [Zero α] [LawfulXor α] (a b c : α) :
    a ^^^ b = c ↔ a = c ^^^ b
    source
    theorem xor_eq_iff_right_eq {α : Type u_1} [XorOp α] [Zero α] [LawfulXor α] (a b c : α) :
    a ^^^ b = c ↔ b = a ^^^ c
    source
    @[simp]
    theorem xor_eq_zero_iff {α : Type u_1} [XorOp α] [Zero α] [LawfulXor α] {a b : α} :
    a ^^^ b = 0 ↔ a = b
    source
    @[simp]
    theorem xor_xor_cancel_comm {α : Type u_1} [XorOp α] [Zero α] [LawfulXor α] (a b : α) :
    a ^^^ b ^^^ a = b
    source
    @[simp]
    theorem xor_xor_cancel_comm_assoc {α : Type u_1} [XorOp α] [Zero α] [LawfulXor α] (a b : α) :
    a ^^^ (b ^^^ a) = b
    source
    @[simp]
    theorem xor_left_eq_self_iff {α : Type u_1} [XorOp α] [Zero α] [LawfulXor α] {a b : α} :
    a ^^^ b = a ↔ b = 0
    source
    @[simp]
    theorem xor_right_eq_self_iff {α : Type u_1} [XorOp α] [Zero α] [LawfulXor α] {a b : α} :
    b ^^^ a = a ↔ b = 0
    source
    @[simp]
    theorem xor_left_eq_id_iff {α : Type u_1} [XorOp α] [Zero α] [LawfulXor α] {a : α} :
    (fun (x : α) => a ^^^ x) = id ↔ a = 0
    source
    @[simp]
    theorem xor_right_eq_id_iff {α : Type u_1} [XorOp α] [Zero α] [LawfulXor α] {a : α} :
    (fun (x : α) => x ^^^ a) = id ↔ a = 0
    source
    @[simp]
    theorem isFixedPt_xor_left_iff {α : Type u_1} [XorOp α] [Zero α] [LawfulXor α] {a b : α} :
    Function.IsFixedPt (fun (x : α) => a ^^^ x) b ↔ a = 0
    source
    @[simp]
    theorem isFixedPt_xor_right_iff {α : Type u_1} [XorOp α] [Zero α] [LawfulXor α] {a b : α} :
    Function.IsFixedPt (fun (x : α) => x ^^^ a) b ↔ a = 0