theorem
proved
tactic proof
sub_eq_add
show as:
view Lean formalization →
formal statement (Lean)
83@[simp] theorem sub_eq_add (u v : F2Power D) : u - v = u + v := rfl
proof body
Tactic-mode proof.
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
109 nsmul := nsmulRec
110 zsmul := zsmulRec
111 sub_eq_add_neg u v := by funext i; rfl
112