neg_eq_self

formal source

  75/-- Negation in characteristic 2 is the identity. -/
  76instance : Neg (F2Power D) := ⟨fun v => v⟩
  77
  78@[simp] theorem neg_eq_self (v : F2Power D) : -v = v := rfl
  79
  80/-- Subtraction reduces to addition in characteristic 2. -/
  81instance : Sub (F2Power D) := ⟨fun u v => u + v⟩
  82
  83@[simp] theorem sub_eq_add (u v : F2Power D) : u - v = u + v := rfl
  84
  85instance : AddCommGroup (F2Power D) where
  86  add := (· + ·)
  87  zero := 0
  88  neg := Neg.neg
  89  add_assoc u v w := by
  90    funext i
  91    show xor (xor (u i) (v i)) (w i) = xor (u i) (xor (v i) (w i))
  92    cases u i <;> cases v i <;> cases w i <;> rfl
  93  zero_add v := by
  94    funext i
  95    show xor false (v i) = v i
  96    cases v i <;> rfl
  97  add_zero v := by
  98    funext i
  99    show xor (v i) false = v i
 100    cases v i <;> rfl
 101  neg_add_cancel v := by
 102    funext i
 103    show xor (v i) (v i) = false
 104    cases v i <;> rfl
 105  add_comm u v := by
 106    funext i
 107    show xor (u i) (v i) = xor (v i) (u i)
 108    cases u i <;> cases v i <;> rfl