mathlib3 documentation

algebra.char_p.two

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 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) :
s.sum (λ (i : ι), f i) ^ 2 = s.sum (λ (i : ι), 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) :
s.sum (λ (i : ι), f i) * s.sum (λ (i : ι), f i) = s.sum (λ (i : ι), 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