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.

source
theorem CharTwo.two_eq_zero {R : Type u_1} [Semiring R] [CharP R 2] :
2 = 0
source
@[simp]
theorem CharTwo.add_self_eq_zero {R : Type u_1} [Semiring R] [CharP R 2] (x : R) :
x + x = 0
source
@[simp]
theorem CharTwo.neg_eq {R : Type u_1} [Ring R] [CharP R 2] (x : R) :
-x = x
source
theorem CharTwo.neg_eq' {R : Type u_1} [Ring R] [CharP R 2] :
Neg.neg = id
source
@[simp]
theorem CharTwo.sub_eq_add {R : Type u_1} [Ring R] [CharP R 2] (x : R) (y : R) :
x - y = x + y
source
theorem CharTwo.sub_eq_add' {R : Type u_1} [Ring R] [CharP R 2] :
HSub.hSub = fun (x x_1 : R) => x + x_1
source
theorem CharTwo.add_sq {R : Type u_1} [CommSemiring R] [CharP R 2] (x : R) (y : R) :
(x + y) ^ 2 = x ^ 2 + y ^ 2
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
theorem neg_one_eq_one_iff {R : Type u_1} [Ring R] [Nontrivial R] :
-1 = 1 ↔ ringChar R = 2
source
@[simp]
theorem orderOf_neg_one {R : Type u_1} [Ring R] [Nontrivial R] :
orderOf (-1) = if ringChar R = 2 then 1 else 2