zero_apply

formal source

  64/-- The zero element: all coordinates `false`. -/
  65instance : Zero (F2Power D) := ⟨fun _ => false⟩
  66
  67@[simp] theorem zero_apply (i : Fin D) : (0 : F2Power D) i = false := rfl
  68
  69/-- Pointwise XOR. -/
  70instance : Add (F2Power D) := ⟨fun u v => fun i => xor (u i) (v i)⟩
  71
  72@[simp] theorem add_apply (u v : F2Power D) (i : Fin D) :
  73    (u + v) i = xor (u i) (v i) := rfl
  74
  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