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.

source

theorem char_two.two_eq_zero {R : Type u_1} [semiring R] [char_p R 2] :

2 = 0

source

@[simp]

theorem char_two.add_self_eq_zero {R : Type u_1} [semiring R] [char_p R 2] (x : R) :

x + x = 0

source

@[simp]

theorem char_two.bit0_eq_zero {R : Type u_1} [semiring R] [char_p R 2] :

bit0 = 0

source

theorem char_two.bit0_apply_eq_zero {R : Type u_1} [semiring R] [char_p R 2] (x : R) :

bit0 x = 0

source

@[simp]

theorem char_two.bit1_eq_one {R : Type u_1} [semiring R] [char_p R 2] :

bit1 = 1

source

theorem char_two.bit1_apply_eq_one {R : Type u_1} [semiring R] [char_p R 2] (x : R) :

bit1 x = 1

source

@[simp]

theorem char_two.neg_eq {R : Type u_1} [ring R] [char_p R 2] (x : R) :

-x = x

source

theorem char_two.neg_eq' {R : Type u_1} [ring R] [char_p R 2] :

has_neg.neg = id

source

@[simp]

theorem char_two.sub_eq_add {R : Type u_1} [ring R] [char_p R 2] (x y : R) :

x - y = x + y

source

theorem char_two.sub_eq_add' {R : Type u_1} [ring R] [char_p R 2] :

has_sub.sub = has_add.add

source

theorem char_two.add_sq {R : Type u_1} [comm_semiring R] [char_p R 2] (x y : R) :

(x + y) ^ 2 = x ^ 2 + y ^ 2

source

theorem char_two.add_mul_self {R : Type u_1} [comm_semiring R] [char_p R 2] (x y : R) :

(x + y) * (x + y) = x * x + y * y

source

theorem char_two.list_sum_sq {R : Type u_1} [comm_semiring R] [char_p R 2] (l : list R) :

l.sum ^ 2 = (list.map (λ (_x : R), _x ^ 2) l).sum

source

theorem char_two.list_sum_mul_self {R : Type u_1} [comm_semiring R] [char_p R 2] (l : list R) :

(l.sum) * l.sum = (list.map (λ (x : R), x * x) l).sum

source

theorem char_two.multiset_sum_sq {R : Type u_1} [comm_semiring R] [char_p R 2] (l : multiset R) :

l.sum ^ 2 = (multiset.map (λ (_x : R), _x ^ 2) l).sum

source

theorem char_two.multiset_sum_mul_self {R : Type u_1} [comm_semiring R] [char_p R 2] (l : multiset R) :

(l.sum) * l.sum = (multiset.map (λ (x : R), x * x) l).sum

source

theorem char_two.sum_sq {R : Type u_1} {ι : Type u_2} [comm_semiring R] [char_p R 2] (s : finset ι) (f : ι → R) :

(∑ (i : ι) in s, f i) ^ 2 = ∑ (i : ι) in s, f i ^ 2

source

theorem char_two.sum_mul_self {R : Type u_1} {ι : Type u_2} [comm_semiring R] [char_p R 2] (s : finset ι) (f : ι → R) :

(∑ (i : ι) in s, f i) * ∑ (i : ι) in s, f i = ∑ (i : ι) in s, (f i) * f i

source

theorem neg_one_eq_one_iff {R : Type u_1} [ring R] [nontrivial R] :

-1 = 1 ↔ ring_char R = 2

source

@[simp]

theorem order_of_neg_one {R : Type u_1} [ring R] [nontrivial R] :

order_of (-1) = ite (ring_char R = 2) 1 2