# mathlibdocumentation

algebra.char_p.two

# 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.two_eq_zero {R : Type u_1} [semiring R] [ 2] :
2 = 0
@[simp]
theorem char_two.add_self_eq_zero {R : Type u_1} [semiring R] [ 2] (x : R) :
x + x = 0
@[simp]
theorem char_two.bit0_eq_zero {R : Type u_1} [semiring R] [ 2] :
theorem char_two.bit0_apply_eq_zero {R : Type u_1} [semiring R] [ 2] (x : R) :
bit0 x = 0
@[simp]
theorem char_two.bit1_eq_one {R : Type u_1} [semiring R] [ 2] :
theorem char_two.bit1_apply_eq_one {R : Type u_1} [semiring R] [ 2] (x : R) :
bit1 x = 1
@[simp]
theorem char_two.neg_eq {R : Type u_1} [ring R] [ 2] (x : R) :
-x = x
theorem char_two.neg_eq' {R : Type u_1} [ring R] [ 2] :
@[simp]
theorem char_two.sub_eq_add {R : Type u_1} [ring R] [ 2] (x y : R) :
x - y = x + y
theorem char_two.sub_eq_add' {R : Type u_1} [ring R] [ 2] :
theorem char_two.add_sq {R : Type u_1} [ 2] (x y : R) :
(x + y) ^ 2 = x ^ 2 + y ^ 2
theorem char_two.add_mul_self {R : Type u_1} [ 2] (x y : R) :
(x + y) * (x + y) = x * x + y * y
theorem char_two.list_sum_sq {R : Type u_1} [ 2] (l : list R) :
l.sum ^ 2 = (list.map (λ (_x : R), _x ^ 2) l).sum
theorem char_two.list_sum_mul_self {R : Type u_1} [ 2] (l : list R) :
l.sum * l.sum = (list.map (λ (x : R), x * x) l).sum
theorem char_two.multiset_sum_sq {R : Type u_1} [ 2] (l : multiset R) :
l.sum ^ 2 = (multiset.map (λ (_x : R), _x ^ 2) l).sum
theorem char_two.multiset_sum_mul_self {R : Type u_1} [ 2] (l : multiset R) :
l.sum * l.sum = (multiset.map (λ (x : R), x * x) l).sum
theorem char_two.sum_sq {R : Type u_1} {ι : Type u_2} [ 2] (s : finset ι) (f : ι → R) :
s.sum (λ (i : ι), f i) ^ 2 = s.sum (λ (i : ι), f i ^ 2)
theorem char_two.sum_mul_self {R : Type u_1} {ι : Type u_2} [ 2] (s : finset ι) (f : ι → R) :
s.sum (λ (i : ι), f i) * s.sum (λ (i : ι), f i) = s.sum (λ (i : ι), f i * f i)
theorem neg_one_eq_one_iff {R : Type u_1} [ring R] [nontrivial R] :
-1 = 1 = 2
@[simp]
theorem order_of_neg_one {R : Type u_1} [ring R] [nontrivial R] :
order_of (-1) = ite = 2) 1 2