Mathlib.Algebra.CharP.Two

CharTwo.two_eq_zero theorem

[CharP R 2] : (2 : R) = 0

Full source

theorem two_eq_zero [CharP R 2] : (2 : R) = 0 := by
  rw [← Nat.cast_two, CharP.cast_eq_zero]

Characteristic Two Implies $2 = 0$

Informal description

In a ring $R$ of characteristic 2, the element $2$ is equal to $0$, i.e., $2 = 0$.

CharTwo.of_one_ne_zero_of_two_eq_zero theorem

(h₁ : (1 : R) ≠ 0) (h₂ : (2 : R) = 0) : CharP R 2

Full source

/-- The only hypotheses required to build a `CharP R 2` instance are `1 ≠ 0` and `2 = 0`. -/
theorem of_one_ne_zero_of_two_eq_zero (h₁ : (1 : R) ≠ 0) (h₂ : (2 : R) = 0) : CharP R 2 where
  cast_eq_zero_iff n := by
    obtain hn | hn := Nat.even_or_odd n
    · simp_rw [hn.two_dvd, iff_true]
      exact natCast_eq_zero_of_even_of_two_eq_zero hn h₂
    · simp_rw [hn.not_two_dvd_nat, iff_false]
      rwa [natCast_eq_one_of_odd_of_two_eq_zero hn h₂]

Characteristic Two Criterion: $1 \neq 0$ and $2 = 0$ Implies $\text{Char}(R) = 2$

Informal description

For any ring $R$, if $1 \neq 0$ and $2 = 0$ in $R$, then $R$ has characteristic 2.

CharTwo.add_self_eq_zero theorem

(x : R) : x + x = 0

Full source

@[scoped simp]
theorem add_self_eq_zero (x : R) : x + x = 0 := by rw [← two_smul R x, two_eq_zero, zero_smul]

Characteristic Two Implies $x + x = 0$ for All Elements

Informal description

In a ring $R$ of characteristic 2, every element $x$ satisfies $x + x = 0$.

CharTwo.two_nsmul theorem

(x : R) : 2 • x = 0

Full source

@[scoped simp]
protected theorem two_nsmul (x : R) : 2 • x = 0 := by rw [two_smul, add_self_eq_zero]

Scalar Multiplication by Two Vanishes in Characteristic Two Rings

Informal description

In a ring $R$ of characteristic 2, the scalar multiplication of any element $x$ by 2 equals zero, i.e., $2 \cdot x = 0$.

CharTwo.neg_eq theorem

(x : R) : -x = x

Full source

@[scoped simp]
theorem neg_eq (x : R) : -x = x := by
  rw [neg_eq_iff_add_eq_zero, add_self_eq_zero]

Negation Equals Identity in Characteristic Two Rings: $-x = x$

Informal description

In a ring $R$ of characteristic 2, the negation of any element $x$ is equal to itself, i.e., $-x = x$.

CharTwo.neg_eq' theorem

: Neg.neg = (id : R → R)

Full source

theorem neg_eq' : Neg.neg = (id : R → R) :=
  funext neg_eq

Negation as Identity in Characteristic Two Rings: $-x = x$

Informal description

In a ring $R$ of characteristic 2, the negation operation is equal to the identity function, i.e., $-x = x$ for all $x \in R$.

CharTwo.sub_eq_add theorem

(x y : R) : x - y = x + y

Full source

@[scoped simp]
theorem sub_eq_add (x y : R) : x - y = x + y := by rw [sub_eq_add_neg, neg_eq]

Subtraction Equals Addition in Characteristic Two Rings: $x - y = x + y$

Informal description

In a ring $R$ of characteristic 2, the subtraction of two elements $x$ and $y$ is equal to their sum, i.e., $x - y = x + y$.

CharTwo.sub_eq_add' theorem

: HSub.hSub = (· + · : R → R → R)

Full source

@[deprecated sub_eq_add (since := "2024-10-24")]
theorem sub_eq_add' : HSub.hSub = (· + · : R → R → R) :=
  funext₂ sub_eq_add

Subtraction Equals Addition in Characteristic Two Rings: $x - y = x + y$

Informal description

In a ring $R$ of characteristic 2, the subtraction operation is equal to the addition operation, i.e., $x - y = x + y$ for all $x, y \in R$.

CharTwo.add_eq_iff_eq_add theorem

{a b c : R} : a + b = c ↔ a = c + b

Full source

theorem add_eq_iff_eq_add {a b c : R} : a + b = c ↔ a = c + b := by
  rw [← sub_eq_iff_eq_add, sub_eq_add]

Addition Equivalence in Characteristic Two Rings: $a + b = c \leftrightarrow a = c + b$

Informal description

In a ring $R$ of characteristic 2, for any elements $a, b, c \in R$, the equation $a + b = c$ holds if and only if $a = c + b$.

CharTwo.two_zsmul theorem

(x : R) : (2 : ℤ) • x = 0

Full source

@[scoped simp]
protected theorem two_zsmul (x : R) : (2 : ℤ) • x = 0 := by
  rw [two_zsmul, add_self_eq_zero]

Integer Scalar Multiplication by 2 Vanishes in Characteristic 2 Rings

Informal description

In a ring $R$ of characteristic 2, the integer scalar multiplication of any element $x$ by 2 equals zero, i.e., $2 \cdot x = 0$.

CharTwo.add_sq theorem

(x y : R) : (x + y) ^ 2 = x ^ 2 + y ^ 2

Full source

theorem add_sq (x y : R) : (x + y) ^ 2 = x ^ 2 + y ^ 2 :=
  add_pow_char _ _ _

Square of Sum in Characteristic 2: $(x + y)^2 = x^2 + y^2$

Informal description

Let $R$ be a commutative semiring of characteristic 2. For any elements $x, y \in R$, the square of their sum equals the sum of their squares, i.e., $(x + y)^2 = x^2 + y^2$.

CharTwo.add_mul_self theorem

(x y : R) : (x + y) * (x + y) = x * x + y * y

Full source

theorem add_mul_self (x y : R) : (x + y) * (x + y) = x * x + y * y := by
  rw [← pow_two, ← pow_two, ← pow_two, add_sq]

Product of Sum Equals Sum of Squares in Characteristic 2

Informal description

Let $R$ be a commutative semiring of characteristic 2. For any elements $x, y \in R$, the product of the sum $(x + y)$ with itself equals the sum of the products $x \cdot x$ and $y \cdot y$, i.e., $(x + y)(x + y) = x^2 + y^2$.

CharTwo.list_sum_sq theorem

(l : List R) : l.sum ^ 2 = (l.map (· ^ 2)).sum

Full source

theorem list_sum_sq (l : List R) : l.sum ^ 2 = (l.map (· ^ 2)).sum :=
  list_sum_pow_char _ _

Square of Sum Equals Sum of Squares in Characteristic 2

Informal description

Let $R$ be a commutative semiring of characteristic 2. For any list $l$ of elements in $R$, the square of the sum of the elements in $l$ is equal to the sum of the squares of the elements in $l$, i.e., $$ \left(\sum_{x \in l} x\right)^2 = \sum_{x \in l} x^2. $$

CharTwo.list_sum_mul_self theorem

(l : List R) : l.sum * l.sum = (List.map (fun x => x * x) l).sum

Full source

theorem list_sum_mul_self (l : List R) : l.sum * l.sum = (List.map (fun x => x * x) l).sum := by
  simp_rw [← pow_two, list_sum_sq]

Square of Sum Equals Sum of Squares for Lists in Characteristic 2

Informal description

Let $R$ be a commutative semiring of characteristic 2. For any list $l$ of elements in $R$, the product of the sum of the elements with itself is equal to the sum of the squares of the elements, i.e., \[ \left(\sum_{x \in l} x\right) \cdot \left(\sum_{x \in l} x\right) = \sum_{x \in l} x^2. \]

CharTwo.multiset_sum_sq theorem

(l : Multiset R) : l.sum ^ 2 = (l.map (· ^ 2)).sum

Full source

theorem multiset_sum_sq (l : Multiset R) : l.sum ^ 2 = (l.map (· ^ 2)).sum :=
  multiset_sum_pow_char _ _

Square of Sum Equals Sum of Squares in Characteristic 2 Multisets

Informal description

Let $R$ be a commutative semiring of characteristic 2. For any multiset $l$ of elements in $R$, the square of the sum of the elements in $l$ is equal to the sum of the squares of the elements in $l$, i.e., \[ \left(\sum_{x \in l} x\right)^2 = \sum_{x \in l} x^2. \]

CharTwo.multiset_sum_mul_self theorem

(l : Multiset R) : l.sum * l.sum = (Multiset.map (fun x => x * x) l).sum

Full source

theorem multiset_sum_mul_self (l : Multiset R) :
    l.sum * l.sum = (Multiset.map (fun x => x * x) l).sum := by simp_rw [← pow_two, multiset_sum_sq]

Square of Sum Equals Sum of Squares in Characteristic 2 Multisets

Informal description

Let $R$ be a commutative semiring of characteristic 2. For any multiset $l$ of elements in $R$, the product of the sum of $l$ with itself equals the sum of the squares of the elements in $l$, i.e., \[ \left(\sum_{x \in l} x\right) \cdot \left(\sum_{x \in l} x\right) = \sum_{x \in l} x^2. \]

CharTwo.sum_sq theorem

(s : Finset ι) (f : ι → R) : (∑ i ∈ s, f i) ^ 2 = ∑ i ∈ s, f i ^ 2

Full source

theorem sum_sq (s : Finset ι) (f : ι → R) : (∑ i ∈ s, f i) ^ 2 = ∑ i ∈ s, f i ^ 2 :=
  sum_pow_char _ _ _

Square of Sum Equals Sum of Squares in Characteristic 2

Informal description

Let $R$ be a commutative semiring of characteristic 2. For any finite set $s$ and any function $f : \iota \to R$, the square of the sum of $f$ over $s$ equals the sum of the squares of $f$ over $s$, i.e., \[ \left(\sum_{i \in s} f(i)\right)^2 = \sum_{i \in s} f(i)^2. \]

CharTwo.sum_mul_self theorem

(s : Finset ι) (f : ι → R) : ((∑ i ∈ s, f i) * ∑ i ∈ s, f i) = ∑ i ∈ s, f i * f i

Full source

theorem sum_mul_self (s : Finset ι) (f : ι → R) :
    ((∑ i ∈ s, f i) * ∑ i ∈ s, f i) = ∑ i ∈ s, f i * f i := by simp_rw [← pow_two, sum_sq]

Product of Sum with Itself Equals Sum of Squares in Characteristic 2

Informal description

Let $R$ be a commutative semiring of characteristic 2. For any finite set $s$ and any function $f : \iota \to R$, the product of the sum of $f$ over $s$ with itself equals the sum of the products $f(i) \cdot f(i)$ over $s$, i.e., \[ \left(\sum_{i \in s} f(i)\right) \cdot \left(\sum_{i \in s} f(i)\right) = \sum_{i \in s} f(i) \cdot f(i). \]

neg_one_eq_one_iff theorem

[Nontrivial R] : (-1 : R) = 1 ↔ ringChar R = 2

Full source

theorem neg_one_eq_one_iff [Nontrivial R] : (-1 : R) = 1 ↔ ringChar R = 2 := by
  refine ⟨fun h => ?_, fun h => @CharTwo.neg_eq _ _ (ringChar.of_eq h) 1⟩
  rw [eq_comm, ← sub_eq_zero, sub_neg_eq_add, ← Nat.cast_one, ← Nat.cast_add] at h
  exact ((Nat.dvd_prime Nat.prime_two).mp (ringChar.dvd h)).resolve_left CharP.ringChar_ne_one

Characterization of Characteristic Two Rings via $-1 = 1$

Informal description

In a nontrivial ring $R$, the equality $-1 = 1$ holds if and only if the ring has characteristic $2$.

orderOf_neg_one theorem

[Nontrivial R] : orderOf (-1 : R) = if ringChar R = 2 then 1 else 2

Full source

@[simp]
theorem orderOf_neg_one [Nontrivial R] : orderOf (-1 : R) = if ringChar R = 2 then 1 else 2 := by
  split_ifs with h
  · rw [neg_one_eq_one_iff.2 h, orderOf_one]
  apply orderOf_eq_prime
  · simp
  simpa [neg_one_eq_one_iff] using h

Order of $-1$ in a Nontrivial Ring: $\text{orderOf}(-1) = 1$ if $\text{char}(R) = 2$, $2$ otherwise

Informal description

In a nontrivial ring $R$, the order of $-1$ is $1$ if the ring has characteristic $2$, and $2$ otherwise. That is, $\text{orderOf}(-1) = \begin{cases} 1 & \text{if } \text{char}(R) = 2, \\ 2 & \text{otherwise.} \end{cases}$

CharP.orderOf_eq_two_iff theorem

[Nontrivial R] [NoZeroDivisors R] (p : ℕ) (hp : p ≠ 2) [CharP R p] {x : R} : orderOf x = 2 ↔ x = -1

Full source

lemma CharP.orderOf_eq_two_iff [Nontrivial R] [NoZeroDivisors R] (p : ℕ)
    (hp : p ≠ 2) [CharP R p] {x : R} : orderOforderOf x = 2 ↔ x = -1 := by
  simp only [orderOf_eq_prime_iff, sq_eq_one_iff, ne_eq, or_and_right, and_not_self, false_or,
    and_iff_left_iff_imp]
  rintro rfl
  exact fun h ↦ hp ((ringChar.eq R p) ▸ (neg_one_eq_one_iff.1 h))

Characterization of Order Two Elements in Rings of Characteristic Not Two: $x$ has order $2$ iff $x = -1$

Informal description

Let $R$ be a nontrivial ring with no zero divisors and characteristic $p \neq 2$. For any element $x \in R$, the order of $x$ is $2$ if and only if $x = -1$.