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} [AddMonoidWithOne R] [CharP R 2] : 2 = 0

theorem CharTwo.of_one_ne_zero_of_two_eq_zero {R : Type u_1} [AddMonoidWithOne R] (h₁ : 1 ≠ 0) (h₂ : 2 = 0) : CharP R 2

The only hypotheses required to build a CharP R 2 instance are 1 ≠ 0 and 2 = 0.

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

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

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

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

@[deprecated CharTwo.sub_eq_add]

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

theorem CharTwo.add_eq_iff_eq_add {R : Type u_1} [Ring R] [CharP R 2] {a : R} {b : R} {c : R} : a + b = c ↔ a = c + b

theorem CharTwo.eq_add_iff_add_eq {R : Type u_1} [Ring R] [CharP R 2] {a : R} {b : R} {c : R} : a = b + c ↔ a + c = b

theorem CharTwo.two_zsmul {R : Type u_1} [Ring R] [CharP R 2] (x : R) : 2 • x = 0

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) : l.sum ^ 2 = (List.map (fun (x : R) => x ^ 2) l).sum

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

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

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

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

theorem CharTwo.sum_mul_self {R : Type u_1} {ι : Type u_2} [CommSemiring R] [CharP R 2] (s : Finset ι) (f : ι → R) : (∑ i ∈ s, f i) * ∑ i ∈ s, f i = ∑ i ∈ s, 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