Lemmas about rings of characteristic two

This file contains results about CharP R 2, in the CharTwo 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 CharTwo.two_eq_zero {R : Type u_1} [Semiring R] [CharP R 2] : 2 = 0

@[simp]

theorem CharTwo.add_self_eq_zero {R : Type u_1} [Semiring R] [CharP R 2] (x : R) : x + x = 0

@[simp]

theorem CharTwo.bit0_eq_zero {R : Type u_1} [Semiring R] [CharP R 2] : bit0 = 0

theorem CharTwo.bit0_apply_eq_zero {R : Type u_1} [Semiring R] [CharP R 2] (x : R) : bit0 x = 0

@[simp]

theorem CharTwo.bit1_eq_one {R : Type u_1} [Semiring R] [CharP R 2] : bit1 = 1

theorem CharTwo.bit1_apply_eq_one {R : Type u_1} [Semiring R] [CharP R 2] (x : R) : bit1 x = 1

@[simp]

theorem CharTwo.neg_eq {R : Type u_1} [Ring R] [CharP R 2] (x : R) : -x = x

theorem CharTwo.neg_eq' {R : Type u_1} [Ring R] [CharP R 2] : Neg.neg = id

@[simp]

theorem CharTwo.sub_eq_add {R : Type u_1} [Ring R] [CharP R 2] (x : R) (y : R) : x - y = x + y

theorem CharTwo.sub_eq_add' {R : Type u_1} [Ring R] [CharP R 2] : HSub.hSub = fun (x x_1 : R) => x + x_1

theorem CharTwo.add_sq {R : Type u_1} [CommSemiring R] [CharP R 2] (x : R) (y : R) : (x + y) ^ 2 = x ^ 2 + y ^ 2

theorem CharTwo.add_mul_self {R : Type u_1} [CommSemiring R] [CharP R 2] (x : R) (y : R) : (x + y) * (x + y) = x * x + y * y

theorem CharTwo.list_sum_sq {R : Type u_1} [CommSemiring R] [CharP R 2] (l : List R) : List.sum l ^ 2 = List.sum (List.map (fun (x : R) => x ^ 2) l)

theorem CharTwo.list_sum_mul_self {R : Type u_1} [CommSemiring R] [CharP R 2] (l : List R) : List.sum l * List.sum l = List.sum (List.map (fun (x : R) => x * x) l)

theorem CharTwo.multiset_sum_sq {R : Type u_1} [CommSemiring R] [CharP R 2] (l : Multiset R) : Multiset.sum l ^ 2 = Multiset.sum (Multiset.map (fun (x : R) => x ^ 2) l)

theorem CharTwo.multiset_sum_mul_self {R : Type u_1} [CommSemiring R] [CharP R 2] (l : Multiset R) : Multiset.sum l * Multiset.sum l = Multiset.sum (Multiset.map (fun (x : R) => x * x) l)

theorem CharTwo.sum_sq {R : Type u_1} {ι : Type u_2} [CommSemiring R] [CharP R 2] (s : Finset ι) (f : ι → R) : (Finset.sum s fun (i : ι) => f i) ^ 2 = Finset.sum s fun (i : ι) => f i ^ 2

theorem CharTwo.sum_mul_self {R : Type u_1} {ι : Type u_2} [CommSemiring R] [CharP R 2] (s : Finset ι) (f : ι → R) : ((Finset.sum s fun (i : ι) => f i) * Finset.sum s fun (i : ι) => f i) = Finset.sum s fun (i : ι) => f i * f i

theorem neg_one_eq_one_iff {R : Type u_1} [Ring R] [Nontrivial R] : -1 = 1 ↔ ringChar R = 2

@[simp]

theorem orderOf_neg_one {R : Type u_1} [Ring R] [Nontrivial R] : orderOf (-1) = if ringChar R = 2 then 1 else 2