Lemmas about rings of characteristic two #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file contains results about
char_p R 2, in the
The lemmas in this file with a
_sq suffix are just special cases of the
elsewhere, with a shorter name for ease of discovery, and no need for a
[fact (prime 2)] argument.