Lemmas about rings of characteristic two #
This file contains results about char_p R 2
, in the char_two
namespace.
The lemmas in this file with a _sq
suffix are just special cases of the _pow_char
lemmas
elsewhere, with a shorter name for ease of discovery, and no need for a [fact (prime 2)]
argument.
theorem
char_two.multiset_sum_mul_self
{R : Type u_1}
[comm_semiring R]
[char_p R 2]
(l : multiset R) :
theorem
char_two.sum_sq
{R : Type u_1}
{ι : Type u_2}
[comm_semiring R]
[char_p R 2]
(s : finset ι)
(f : ι → R) :
@[simp]