Documentation

Mathlib.Algebra.CharP.Two

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] :
Sub.sub = fun x x_1 => 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 => 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 => 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 => x ^ 2) 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