characteristic two

Stream: Is there code for X?

[Eric Wieser]

Do we have this anywhere?

lemma char_two_neg {R} [ring R] [char_p R 2] (x : R) : -x = x :=
by rw [neg_eq_iff_add_eq_zero, ←two_smul ℕ x, nsmul_eq_smul_cast R 2 x, char_p.cast_eq_zero,
  zero_smul]

lemma char_two_sub {R} [ring R] [char_p R 2] (x y : R) : x - y = x + y :=
by rw [sub_eq_add_neg, char_two_neg]