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.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.two_eq_zero {R : Type u_1} [AddMonoidWithOne R] [CharP R 2] : 2 = 0

theorem CharTwo.natCast_eq_ite {R : Type u_1} [AddMonoidWithOne R] [CharP R 2] (n : ℕ) : ↑n = if Even n then 0 else 1

@[simp]

theorem CharTwo.range_natCast {R : Type u_1} [AddMonoidWithOne R] [CharP R 2] : Set.range Nat.cast = {0, 1}

theorem CharTwo.natCast_cases (R : Type u_1) [AddMonoidWithOne R] [CharP R 2] (n : ℕ) : ↑n = 0 ∨ ↑n = 1

theorem CharTwo.natCast_eq_mod {R : Type u_1} [AddMonoidWithOne R] [CharP R 2] (n : ℕ) : ↑n = ↑(n % 2)

theorem CharTwo.ofNat_eq_mod {R : Type u_1} [AddMonoidWithOne R] [CharP R 2] (n : ℕ) [n.AtLeastTwo] : OfNat.ofNat n = ↑(OfNat.ofNat n % 2)

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.add_cancel_left {R : Type u_1} [Semiring R] [CharP R 2] (a b : R) : a + (a + b) = b

theorem CharTwo.add_cancel_right {R : Type u_1} [Semiring R] [CharP R 2] (a b : R) : a + b + b = a

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 y : R) : x - y = x + y

theorem CharTwo.add_eq_iff_eq_add {R : Type u_1} [Ring R] [CharP R 2] {a b 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 b 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_eq_zero {R : Type u_1} [Ring R] [CharP R 2] {a b : R} : a + b = 0 ↔ a = b

theorem CharTwo.intCast_eq_ite {R : Type u_1} [Ring R] [CharP R 2] (n : ℤ) : ↑n = if Even n then 0 else 1

@[simp]

theorem CharTwo.range_intCast {R : Type u_1} [Ring R] [CharP R 2] : Set.range Int.cast = {0, 1}

theorem CharTwo.intCast_cases (R : Type u_1) [Ring R] [CharP R 2] (n : ℤ) : ↑n = 0 ∨ ↑n = 1

theorem CharTwo.intCast_eq_mod {R : Type u_1} [Ring R] [CharP R 2] (n : ℤ) : ↑n = ↑(n % 2)

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

theorem CharTwo.add_mul_self {R : Type u_1} [CommSemiring R] [CharP R 2] (x 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 CharTwo.sq_injective {R : Type u_1} [CommRing R] [CharP R 2] [NoZeroDivisors R] : Function.Injective fun (x : R) => x ^ 2

theorem CharTwo.sq_inj {R : Type u_1} [CommRing R] [CharP R 2] [NoZeroDivisors R] {x y : R} : x ^ 2 = y ^ 2 ↔ x = y

@[deprecated CharTwo.sq_injective (since := "2026-02-05")]

theorem CharTwo.CommRing.sq_injective {R : Type u_1} [CommRing R] [CharP R 2] [NoZeroDivisors R] : Function.Injective fun (x : R) => x ^ 2

Alias of CharTwo.sq_injective.

@[deprecated CharTwo.sq_inj (since := "2026-02-05")]

theorem CharTwo.CommRing.sq_inj {R : Type u_1} [CommRing R] [CharP R 2] [NoZeroDivisors R] {x y : R} : x ^ 2 = y ^ 2 ↔ x = y

Alias of CharTwo.sq_inj.

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