LawfulXor equivalences

def Equiv.xor {α : Type u_1} [XorOp α] [Zero α] [LawfulXor α] (a : α) : Perm α

XorOp.xor as a permutation.

Equations

• Equiv.xor a = { toFun := fun (x : α) => a ^^^ x, invFun := fun (x : α) => a ^^^ x, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Equiv.xor_apply {α : Type u_1} [XorOp α] [Zero α] [LawfulXor α] (a x✝ : α) : (Equiv.xor a) x✝ = a ^^^ x✝

@[simp]

theorem Equiv.xor_symm {α : Type u_1} [XorOp α] [Zero α] [LawfulXor α] {a : α} : Equiv.symm (Equiv.xor a) = Equiv.xor a

theorem Equiv.xor_involutive {α : Type u_1} [XorOp α] [Zero α] [LawfulXor α] (a : α) : Function.Involutive ⇑(Equiv.xor a)

@[simp]

theorem Equiv.xor_zero {α : Type u_1} [XorOp α] [Zero α] [LawfulXor α] : Equiv.xor 0 = 1

@[simp]

theorem Equiv.xor_eq_one_iff {α : Type u_1} [XorOp α] [Zero α] [LawfulXor α] {a : α} : Equiv.xor a = 1 ↔ a = 0

theorem Equiv.isFixedPt_xor {α : Type u_1} [XorOp α] [Zero α] [LawfulXor α] {a b : α} : Function.IsFixedPt (⇑(Equiv.xor a)) b ↔ a = 0

@[simp]

theorem Equiv.xor_trans_xor {α : Type u_1} [XorOp α] [Zero α] [LawfulXor α] {a b : α} : Equiv.trans (Equiv.xor b) (Equiv.xor a) = Equiv.xor (a ^^^ b)