Mathlib.Algebra.Ring.Commute

Commute.add_right theorem

[Distrib R] {a b c : R} : Commute a b → Commute a c → Commute a (b + c)

Full source

@[simp]
theorem add_right [Distrib R] {a b c : R} : Commute a b → Commute a c → Commute a (b + c) :=
  SemiconjBy.add_right

Right Sum of Commuting Elements Commutes with Third Element

Informal description

Let $R$ be a type with addition and multiplication satisfying distributivity. For any elements $a, b, c \in R$, if $a$ commutes with $b$ and $a$ commutes with $c$, then $a$ commutes with $b + c$. That is, $a * (b + c) = (b + c) * a$.

Commute.add_left theorem

[Distrib R] {a b c : R} : Commute a c → Commute b c → Commute (a + b) c

Full source

@[simp]
theorem add_left [Distrib R] {a b c : R} : Commute a c → Commute b c → Commute (a + b) c :=
  SemiconjBy.add_left

Sum of Commuting Elements Commutes with Third Element

Informal description

Let $ R $ be a type equipped with addition and multiplication satisfying distributivity. For any elements $ a, b, c \in R $, if $ a $ commutes with $ c $ and $ b $ commutes with $ c $, then $ a + b $ commutes with $ c $. That is, $(a + b) * c = c * (a + b)$.

Commute.mul_self_sub_mul_self_eq theorem

[NonUnitalNonAssocRing R] {a b : R} (h : Commute a b) : a * a - b * b = (a + b) * (a - b)

Full source

/-- Representation of a difference of two squares of commuting elements as a product. -/
theorem mul_self_sub_mul_self_eq [NonUnitalNonAssocRing R] {a b : R} (h : Commute a b) :
    a * a - b * b = (a + b) * (a - b) := by
  rw [add_mul, mul_sub, mul_sub, h.eq, sub_add_sub_cancel]

Difference of Squares Identity for Commuting Elements: $a^2 - b^2 = (a+b)(a-b)$

Informal description

Let $R$ be a non-unital non-associative ring, and let $a, b \in R$ be elements that commute (i.e., $ab = ba$). Then the difference of squares can be expressed as: \[ a^2 - b^2 = (a + b)(a - b) \]

Commute.mul_self_sub_mul_self_eq' theorem

[NonUnitalNonAssocRing R] {a b : R} (h : Commute a b) : a * a - b * b = (a - b) * (a + b)

Full source

theorem mul_self_sub_mul_self_eq' [NonUnitalNonAssocRing R] {a b : R} (h : Commute a b) :
    a * a - b * b = (a - b) * (a + b) := by
  rw [mul_add, sub_mul, sub_mul, h.eq, sub_add_sub_cancel]

Difference of Squares Identity for Commuting Elements in a Non-Unital Non-Associative Ring

Informal description

Let $R$ be a non-unital non-associative ring, and let $a, b \in R$ be elements that commute (i.e., $a * b = b * a$). Then the difference of squares can be expressed as: $$a^2 - b^2 = (a - b)(a + b).$$

Commute.mul_self_eq_mul_self_iff theorem

[NonUnitalNonAssocRing R] [NoZeroDivisors R] {a b : R} (h : Commute a b) : a * a = b * b ↔ a = b ∨ a = -b

Full source

theorem mul_self_eq_mul_self_iff [NonUnitalNonAssocRing R] [NoZeroDivisors R] {a b : R}
    (h : Commute a b) : a * a = b * b ↔ a = b ∨ a = -b := by
  rw [← sub_eq_zero, h.mul_self_sub_mul_self_eq, mul_eq_zero, or_comm, sub_eq_zero,
    add_eq_zero_iff_eq_neg]

Square Equality for Commuting Elements: $a^2 = b^2 \leftrightarrow a = b \lor a = -b$

Informal description

Let $R$ be a non-unital non-associative ring with no zero divisors, and let $a, b \in R$ be commuting elements (i.e., $ab = ba$). Then $a^2 = b^2$ if and only if $a = b$ or $a = -b$.

Commute.neg_right theorem

: Commute a b → Commute a (-b)

Full source

theorem neg_right : Commute a b → Commute a (-b) :=
  SemiconjBy.neg_right

Negation Preserves Commutation: $\text{Commute}(a, b) \to \text{Commute}(a, -b)$

Informal description

For any elements $a$ and $b$ in a multiplicative structure with distributive negation, if $a$ and $b$ commute (i.e., $a * b = b * a$), then $a$ and $-b$ also commute (i.e., $a * (-b) = (-b) * a$).

Commute.neg_right_iff theorem

: Commute a (-b) ↔ Commute a b

Full source

@[simp]
theorem neg_right_iff : CommuteCommute a (-b) ↔ Commute a b :=
  SemiconjBy.neg_right_iff

Negation Preserves Commutation: $\text{Commute}(a, -b) \leftrightarrow \text{Commute}(a, b)$

Informal description

For elements $a$ and $b$ in a multiplicative structure with distributive negation, the elements $a$ and $-b$ commute if and only if $a$ and $b$ commute. That is, $a * (-b) = (-b) * a$ if and only if $a * b = b * a$.

Commute.neg_left theorem

: Commute a b → Commute (-a) b

Full source

theorem neg_left : Commute a b → Commute (-a) b :=
  SemiconjBy.neg_left

Negation Preserves Commutation: $\text{Commute}(a, b) \to \text{Commute}(-a, b)$

Informal description

For any elements $a$ and $b$ in a multiplicative structure with distributive negation, if $a$ and $b$ commute (i.e., $a * b = b * a$), then $-a$ and $b$ also commute (i.e., $-a * b = b * -a$).

Commute.neg_left_iff theorem

: Commute (-a) b ↔ Commute a b

Full source

@[simp]
theorem neg_left_iff : CommuteCommute (-a) b ↔ Commute a b :=
  SemiconjBy.neg_left_iff

Negation Preserves Commutation: $\text{Commute}(-a, b) \leftrightarrow \text{Commute}(a, b)$

Informal description

For elements $a$ and $b$ in a multiplicative structure with distributive negation, the elements $-a$ and $b$ commute if and only if $a$ and $b$ commute. That is, $-a * b = b * -a$ if and only if $a * b = b * a$.

Commute.neg_one_right theorem

(a : R) : Commute a (-1)

Full source

theorem neg_one_right (a : R) : Commute a (-1) :=
  SemiconjBy.neg_one_right a

Negation Commutes with Any Element: $a * (-1) = (-1) * a$

Informal description

For any element $a$ in a ring $R$, the element $-1$ commutes with $a$, i.e., $a * (-1) = (-1) * a$.

Commute.neg_one_left theorem

(a : R) : Commute (-1) a

Full source

theorem neg_one_left (a : R) : Commute (-1) a :=
  SemiconjBy.neg_one_left a

Negation Commutes with Any Element: $-1 * a = a * -1$

Informal description

For any element $a$ in a multiplicative structure $R$ with distributive negation, the element $-1$ commutes with $a$, i.e., $-1 * a = a * -1$.

Commute.sub_right theorem

: Commute a b → Commute a c → Commute a (b - c)

Full source

@[simp]
theorem sub_right : Commute a b → Commute a c → Commute a (b - c) :=
  SemiconjBy.sub_right

Right Subtraction Preserves Commutativity: $a * (b - c) = (b - c) * a$ under commuting conditions

Informal description

For any elements $a$, $b$, and $c$ in a non-unital non-associative ring, if $a$ commutes with $b$ and $a$ commutes with $c$, then $a$ commutes with $b - c$, i.e., $a * (b - c) = (b - c) * a$.

Commute.sub_left theorem

: Commute a c → Commute b c → Commute (a - b) c

Full source

@[simp]
theorem sub_left : Commute a c → Commute b c → Commute (a - b) c :=
  SemiconjBy.sub_left

Left Subtraction Preserves Commutativity: $(a - b) * c = c * (a - b)$ when $a$ and $b$ commute with $c$

Informal description

For any elements $ a, b, c $ in a non-unital non-associative ring, if $ a $ commutes with $ c $ and $ b $ commutes with $ c $, then $ a - b $ commutes with $ c $, i.e., $(a - b) * c = c * (a - b)$.

Commute.sq_sub_sq theorem

(h : Commute a b) : a ^ 2 - b ^ 2 = (a + b) * (a - b)

Full source

protected lemma sq_sub_sq (h : Commute a b) : a ^ 2 - b ^ 2 = (a + b) * (a - b) := by
  rw [sq, sq, h.mul_self_sub_mul_self_eq]

Difference of Squares Identity for Commuting Elements: $a^2 - b^2 = (a+b)(a-b)$

Informal description

For any two commuting elements $a$ and $b$ in a non-unital non-associative ring, the difference of their squares equals the product of their sum and difference, i.e., \[ a^2 - b^2 = (a + b)(a - b). \]

Commute.sq_eq_sq_iff_eq_or_eq_neg theorem

(h : Commute a b) : a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b

Full source

protected lemma sq_eq_sq_iff_eq_or_eq_neg (h : Commute a b) : a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b := by
  rw [← sub_eq_zero, h.sq_sub_sq, mul_eq_zero, add_eq_zero_iff_eq_neg, sub_eq_zero, or_comm]

Squares of Commuting Elements are Equal iff Elements are Equal or Negatives: $a^2 = b^2 \leftrightarrow a = b \lor a = -b$

Informal description

For any two commuting elements $a$ and $b$ in a ring, the squares of $a$ and $b$ are equal if and only if $a = b$ or $a = -b$, i.e., \[ a^2 = b^2 \leftrightarrow a = b \lor a = -b. \]

neg_one_pow_eq_or theorem

: ∀ n : ℕ, (-1 : R) ^ n = 1 ∨ (-1 : R) ^ n = -1

Full source

lemma neg_one_pow_eq_or : ∀ n : ℕ, (-1 : R) ^ n = 1 ∨ (-1 : R) ^ n = -1
  | 0 => Or.inl (pow_zero _)
  | n + 1 => (neg_one_pow_eq_or n).symm.imp
    (fun h ↦ by rw [pow_succ, h, neg_one_mul, neg_neg])
    (fun h ↦ by rw [pow_succ, h, one_mul])

Alternating Powers of Negative One: $(-1)^n = \pm 1$

Informal description

For any natural number $n$, the $n$-th power of $-1$ in a ring $R$ is either $1$ or $-1$, i.e., $(-1)^n = 1$ or $(-1)^n = -1$.

neg_pow theorem

(a : R) (n : ℕ) : (-a) ^ n = (-1) ^ n * a ^ n

Full source

lemma neg_pow (a : R) (n : ℕ) : (-a) ^ n = (-1) ^ n * a ^ n :=
  neg_one_mul a ▸ (Commute.neg_one_left a).mul_pow n

Power of Negative Element: $(-a)^n = (-1)^n a^n$

Informal description

For any element $a$ in a ring $R$ and any natural number $n$, the $n$-th power of $-a$ equals the product of $(-1)^n$ and $a^n$, i.e., $(-a)^n = (-1)^n \cdot a^n$.

neg_pow' theorem

(a : R) (n : ℕ) : (-a) ^ n = a ^ n * (-1) ^ n

Full source

lemma neg_pow' (a : R) (n : ℕ) : (-a) ^ n = a ^ n * (-1) ^ n :=
  mul_neg_one a ▸ (Commute.neg_one_right a).mul_pow n

Power of Negative Element: $(-a)^n = a^n \cdot (-1)^n$

Informal description

For any element $a$ in a ring $R$ and any natural number $n$, the $n$-th power of $-a$ equals the product of the $n$-th power of $a$ and the $n$-th power of $-1$, i.e., $(-a)^n = a^n \cdot (-1)^n$.

neg_sq theorem

(a : R) : (-a) ^ 2 = a ^ 2

Full source

lemma neg_sq (a : R) : (-a) ^ 2 = a ^ 2 := by simp [sq]

Square of Negative Element: $(-a)^2 = a^2$

Informal description

For any element $a$ in a ring $R$, the square of $-a$ equals the square of $a$, i.e., $(-a)^2 = a^2$.

neg_one_sq theorem

: (-1 : R) ^ 2 = 1

Full source

lemma neg_one_sq : (-1 : R) ^ 2 = 1 := by simp [neg_sq, one_pow]

Square of Negative One: $(-1)^2 = 1$

Informal description

For any ring $R$, the square of the additive inverse of the multiplicative identity is equal to the multiplicative identity, i.e., $(-1)^2 = 1$.

neg_one_pow_mul_eq_zero_iff theorem

: (-1) ^ n * a = 0 ↔ a = 0

Full source

@[simp] lemma neg_one_pow_mul_eq_zero_iff : (-1) ^ n * a = 0 ↔ a = 0 := by
  rcases neg_one_pow_eq_or R n with h | h <;> simp [h]

Zero Product Property for $(-1)^n \cdot a$: $(-1)^n \cdot a = 0 \leftrightarrow a = 0$

Informal description

For any natural number $n$ and any element $a$ in a ring $R$, the product of $(-1)^n$ and $a$ is zero if and only if $a$ is zero, i.e., $(-1)^n \cdot a = 0 \leftrightarrow a = 0$.

mul_neg_one_pow_eq_zero_iff theorem

: a * (-1) ^ n = 0 ↔ a = 0

Full source

@[simp] lemma mul_neg_one_pow_eq_zero_iff : a * (-1) ^ n = 0 ↔ a = 0 := by
  obtain h | h := neg_one_pow_eq_or R n <;> simp [h]

Zero Product Property with Alternating Sign: $a \cdot (-1)^n = 0 \leftrightarrow a = 0$

Informal description

For any element $a$ in a ring $R$ and any natural number $n$, the product $a \cdot (-1)^n$ equals zero if and only if $a$ itself is zero, i.e., $a \cdot (-1)^n = 0 \leftrightarrow a = 0$.

neg_one_pow_eq_pow_mod_two theorem

(n : ℕ) : (-1 : R) ^ n = (-1) ^ (n % 2)

Full source

lemma neg_one_pow_eq_pow_mod_two (n : ℕ) : (-1 : R) ^ n = (-1) ^ (n % 2) := by
  rw [← Nat.mod_add_div n 2, pow_add, pow_mul]; simp [sq]

Alternating Sign Power Law: $(-1)^n = (-1)^{n \bmod 2}$

Informal description

For any natural number $n$ and any ring $R$, the $n$-th power of $-1$ in $R$ equals the $k$-th power of $-1$, where $k$ is the remainder when $n$ is divided by 2, i.e., $(-1)^n = (-1)^{n \bmod 2}$.

sq_eq_one_iff theorem

: a ^ 2 = 1 ↔ a = 1 ∨ a = -1

Full source

@[simp] lemma sq_eq_one_iff : a ^ 2 = 1 ↔ a = 1 ∨ a = -1 := by
  rw [← (Commute.one_right a).sq_eq_sq_iff_eq_or_eq_neg, one_pow]

Square Equals One iff Element is One or Negative One: $a^2 = 1 \leftrightarrow a = 1 \lor a = -1$

Informal description

For any element $a$ in a ring, the square of $a$ equals $1$ if and only if $a$ is equal to $1$ or $-1$, i.e., $a^2 = 1 \leftrightarrow a = 1 \lor a = -1$.

sq_ne_one_iff theorem

: a ^ 2 ≠ 1 ↔ a ≠ 1 ∧ a ≠ -1

Full source

lemma sq_ne_one_iff : a ^ 2 ≠ 1a ^ 2 ≠ 1 ↔ a ≠ 1 ∧ a ≠ -1 := sq_eq_one_iff.not.trans not_or

Square Not Equal to One iff Not One or Negative One: $a^2 \neq 1 \leftrightarrow a \neq 1 \land a \neq -1$

Informal description

For any element $a$ in a ring, the square of $a$ is not equal to $1$ if and only if $a$ is neither $1$ nor $-1$, i.e., $a^2 \neq 1 \leftrightarrow a \neq 1 \land a \neq -1$.

mul_self_sub_mul_self theorem

[NonUnitalNonAssocCommRing R] (a b : R) : a * a - b * b = (a + b) * (a - b)

Full source

/-- Representation of a difference of two squares in a commutative ring as a product. -/
theorem mul_self_sub_mul_self [NonUnitalNonAssocCommRing R] (a b : R) :
    a * a - b * b = (a + b) * (a - b) :=
  (Commute.all a b).mul_self_sub_mul_self_eq

Difference of Squares Identity in Non-unital Non-associative Commutative Rings: $a^2 - b^2 = (a+b)(a-b)$

Informal description

Let $R$ be a non-unital non-associative commutative ring. For any elements $a, b \in R$, the difference of squares can be expressed as: \[ a^2 - b^2 = (a + b)(a - b) \]

mul_self_sub_one theorem

[NonAssocRing R] (a : R) : a * a - 1 = (a + 1) * (a - 1)

Full source

theorem mul_self_sub_one [NonAssocRing R] (a : R) : a * a - 1 = (a + 1) * (a - 1) := by
  rw [← (Commute.one_right a).mul_self_sub_mul_self_eq, mul_one]

Difference of Squares Identity: $a^2 - 1 = (a+1)(a-1)$ in a Non-Associative Ring

Informal description

For any element $a$ in a non-associative ring $R$, the difference of squares identity holds: \[ a^2 - 1 = (a + 1)(a - 1) \]

mul_self_eq_mul_self_iff theorem

[NonUnitalNonAssocCommRing R] [NoZeroDivisors R] {a b : R} : a * a = b * b ↔ a = b ∨ a = -b

Full source

theorem mul_self_eq_mul_self_iff [NonUnitalNonAssocCommRing R] [NoZeroDivisors R] {a b : R} :
    a * a = b * b ↔ a = b ∨ a = -b :=
  (Commute.all a b).mul_self_eq_mul_self_iff

Square Equality in Commutative Rings: $a^2 = b^2 \leftrightarrow a = b \lor a = -b$

Informal description

Let $R$ be a non-unital non-associative commutative ring with no zero divisors. For any elements $a, b \in R$, we have $a^2 = b^2$ if and only if $a = b$ or $a = -b$.

mul_self_eq_one_iff theorem

[NonAssocRing R] [NoZeroDivisors R] {a : R} : a * a = 1 ↔ a = 1 ∨ a = -1

Full source

theorem mul_self_eq_one_iff [NonAssocRing R] [NoZeroDivisors R] {a : R} :
    a * a = 1 ↔ a = 1 ∨ a = -1 := by
  rw [← (Commute.one_right a).mul_self_eq_mul_self_iff, mul_one]

Square Equals One iff Element is One or Negative One in Non-Associative Ring

Informal description

Let $R$ be a non-associative ring with no zero divisors. For any element $a \in R$, we have $a^2 = 1$ if and only if $a = 1$ or $a = -1$.

sq_sub_sq theorem

(a b : R) : a ^ 2 - b ^ 2 = (a + b) * (a - b)

Full source

lemma sq_sub_sq (a b : R) : a ^ 2 - b ^ 2 = (a + b) * (a - b) := (Commute.all a b).sq_sub_sq

Difference of Squares Identity: $a^2 - b^2 = (a+b)(a-b)$

Informal description

For any elements $a$ and $b$ in a ring $R$, the difference of their squares equals the product of their sum and difference, i.e., \[ a^2 - b^2 = (a + b)(a - b). \]

sub_sq theorem

(a b : R) : (a - b) ^ 2 = a ^ 2 - 2 * a * b + b ^ 2

Full source

lemma sub_sq (a b : R) : (a - b) ^ 2 = a ^ 2 - 2 * a * b + b ^ 2 := by
  rw [sub_eq_add_neg, add_sq, neg_sq, mul_neg, ← sub_eq_add_neg]

Square of Difference Formula: $(a - b)^2 = a^2 - 2ab + b^2$

Informal description

For any elements $a$ and $b$ in a commutative ring $R$, the square of their difference $(a - b)^2$ equals $a^2 - 2ab + b^2$.

sub_sq' theorem

(a b : R) : (a - b) ^ 2 = a ^ 2 + b ^ 2 - 2 * a * b

Full source

lemma sub_sq' (a b : R) : (a - b) ^ 2 = a ^ 2 + b ^ 2 - 2 * a * b := by
  rw [sub_eq_add_neg, add_sq', neg_sq, mul_neg, ← sub_eq_add_neg]

Square of Difference Formula (Rearranged): $(a - b)^2 = a^2 + b^2 - 2ab$

Informal description

For any elements $a$ and $b$ in a commutative ring $R$, the square of their difference $(a - b)^2$ equals $a^2 + b^2 - 2ab$.

sub_sq_comm theorem

(a b : R) : (a - b) ^ 2 = (b - a) ^ 2

Full source

lemma sub_sq_comm (a b : R) : (a - b) ^ 2 = (b - a) ^ 2 := by
  rw [sub_sq', mul_right_comm, add_comm, sub_sq']

Square of Difference is Commutative: $(a - b)^2 = (b - a)^2$

Informal description

For any elements $a$ and $b$ in a commutative ring $R$, the square of their difference $(a - b)^2$ is equal to the square of the reverse difference $(b - a)^2$.

sq_eq_sq_iff_eq_or_eq_neg theorem

: a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b

Full source

lemma sq_eq_sq_iff_eq_or_eq_neg : a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b :=
  (Commute.all a b).sq_eq_sq_iff_eq_or_eq_neg

Square Equality in Commutative Rings: $a^2 = b^2 \leftrightarrow a = b \lor a = -b$

Informal description

For any two elements $a$ and $b$ in a commutative ring with no zero divisors, the squares of $a$ and $b$ are equal if and only if $a = b$ or $a = -b$, i.e., \[ a^2 = b^2 \leftrightarrow a = b \lor a = -b. \]

Units.sq_eq_sq_iff_eq_or_eq_neg theorem

{a b : Rˣ} : a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b

Full source

protected lemma sq_eq_sq_iff_eq_or_eq_neg {a b : Rˣ} : a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b := by
  simp_rw [Units.ext_iff, val_pow_eq_pow_val, sq_eq_sq_iff_eq_or_eq_neg, Units.val_neg]

Square Equality for Units: $a^2 = b^2 \leftrightarrow a = b \lor a = -b$

Informal description

For any two units $a$ and $b$ in a commutative ring $R$ with no zero divisors, the squares of $a$ and $b$ are equal if and only if $a = b$ or $a = -b$. In other words, $a^2 = b^2 \leftrightarrow (a = b \lor a = -b)$.

Units.inv_eq_self_iff theorem

[Ring R] [NoZeroDivisors R] (u : Rˣ) : u⁻¹ = u ↔ u = 1 ∨ u = -1

Full source

/-- In the unit group of an integral domain, a unit is its own inverse iff the unit is one or
  one's additive inverse. -/
theorem inv_eq_self_iff [Ring R] [NoZeroDivisors R] (u : Rˣ) : u⁻¹u⁻¹ = u ↔ u = 1 ∨ u = -1 := by
  rw [inv_eq_iff_mul_eq_one]
  simp only [Units.ext_iff]
  push_cast
  exact mul_self_eq_one_iff

Unit is Self-Inverse iff it is One or Negative One in a Ring without Zero Divisors

Informal description

Let $R$ be a ring with no zero divisors, and let $u$ be a unit in $R$. Then the inverse of $u$ equals $u$ if and only if $u$ is the multiplicative identity $1$ or its additive inverse $-1$, i.e., $u^{-1} = u \leftrightarrow u = 1 \lor u = -1$.

Ring.instBracket instance

: Bracket R R

Full source

instance (priority := 100) instBracket : Bracket R R := ⟨fun x y => x * y - y * x⟩

The Commutator Bracket on a Ring

Informal description

For any ring $R$, there is a canonical bracket operation $\lbrack \cdot, \cdot \rbrack : R \times R \to R$ defined by $\lbrack x, y \rbrack = x y - y x$.

Ring.lie_def theorem

(x y : R) : ⁅x, y⁆ = x * y - y * x

Full source

theorem lie_def (x y : R) : ⁅x, y⁆ = x * y - y * x := rfl

Commutator Bracket Definition: $\lbrack x, y \rbrack = xy - yx$

Informal description

For any elements $x$ and $y$ in a ring $R$, the commutator bracket $\lbrack x, y \rbrack$ is equal to $x y - y x$.

commute_iff_lie_eq theorem

{x y : R} : Commute x y ↔ ⁅x, y⁆ = 0

Full source

theorem commute_iff_lie_eq {x y : R} : CommuteCommute x y ↔ ⁅x, y⁆ = 0 := sub_eq_zero.symm

Commutativity Criterion via Commutator Bracket: $\text{Commute}(x,y) \leftrightarrow \lbrack x, y \rbrack = 0$

Informal description

Two elements $x$ and $y$ in a ring $R$ commute if and only if their commutator bracket $\lbrack x, y \rbrack = x y - y x$ equals zero. That is, $x$ and $y$ commute if and only if $\lbrack x, y \rbrack = 0$.

Commute.lie_eq theorem

{x y : R} (h : Commute x y) : ⁅x, y⁆ = 0

Full source

theorem Commute.lie_eq {x y : R} (h : Commute x y) : ⁅x, y⁆ = 0 := sub_eq_zero_of_eq h

Commutativity Implies Zero Commutator Bracket

Informal description

For any two elements $x$ and $y$ in a ring $R$ that commute (i.e., $x * y = y * x$), their commutator bracket satisfies $\lbrack x, y \rbrack = 0$.