# mathlibdocumentation

algebra.group.commute

# Commuting pairs of elements in monoids

We define the predicate commute a b := a * b = b * a and provide some operations on terms (h : commute a b). E.g., if a, b, and c are elements of a semiring, and that hb : commute a b and hc : commute a c. Then hb.pow_left 5 proves commute (a ^ 5) b and (hb.pow_right 2).add_right (hb.mul_right hc) proves commute a (b ^ 2 + b * c).

Lean does not immediately recognise these terms as equations, so for rewriting we need syntax like rw [(hb.pow_left 5).eq] rather than just rw [hb.pow_left 5].

This file defines only a few operations (mul_left, inv_right, etc). Other operations (pow_right, field inverse etc) are in the files that define corresponding notions.

## Implementation details

Most of the proofs come from the properties of semiconj_by.

S → S → Prop

Two elements additively commute if a + b = b + a

def commute {S : Type u_1} [has_mul S] :
S → S → Prop

Two elements commute if a * b = b * a.

Equations
• b = b b
theorem commute.eq {S : Type u_1} [has_mul S] {a b : S} :
ba * b = b * a

Equality behind commute a b; useful for rewriting.

theorem add_commute.eq {S : Type u_1} [has_add S] {a b : S} :
ba + b = b + a

@[simp]
theorem add_commute.refl {S : Type u_1} [has_add S] (a : S) :
a

@[simp]
theorem commute.refl {S : Type u_1} [has_mul S] (a : S) :
a

Any element commutes with itself.

theorem add_commute.symm {S : Type u_1} [has_add S] {a b : S} :
b a

theorem commute.symm {S : Type u_1} [has_mul S] {a b : S} :
b a

If a commutes with b, then b commutes with a.

theorem add_commute.symm_iff {S : Type u_1} [has_add S] {a b : S} :
b a

theorem commute.symm_iff {S : Type u_1} [has_mul S] {a b : S} :
b a

@[simp]
theorem commute.mul_right {S : Type u_1} [semigroup S] {a b c : S} :
b c (b * c)

If a commutes with both b and c, then it commutes with their product.

@[simp]
theorem add_commute.add_right {S : Type u_1} {a b c : S} :
b c (b + c)

@[simp]
theorem commute.mul_left {S : Type u_1} [semigroup S] {a b c : S} :
c ccommute (a * b) c

If both a and b commute with c, then their product commutes with c.

@[simp]
theorem add_commute.add_left {S : Type u_1} {a b c : S} :
c cadd_commute (a + b) c

theorem commute.right_comm {S : Type u_1} [semigroup S] {b c : S} (h : c) (a : S) :
(a * b) * c = (a * c) * b

theorem add_commute.right_comm {S : Type u_1} {b c : S} (h : c) (a : S) :
a + b + c = a + c + b

theorem add_commute.left_comm {S : Type u_1} {a b : S} (h : b) (c : S) :
a + (b + c) = b + (a + c)

theorem commute.left_comm {S : Type u_1} [semigroup S] {a b : S} (h : b) (c : S) :
a * b * c = b * a * c

theorem commute.all {S : Type u_1} (a b : S) :
b

theorem add_commute.all {S : Type u_1} (a b : S) :
b

@[simp]
theorem commute.one_right {M : Type u_1} [monoid M] (a : M) :
1

@[simp]
theorem add_commute.zero_right {M : Type u_1} [add_monoid M] (a : M) :
0

@[simp]
theorem commute.one_left {M : Type u_1} [monoid M] (a : M) :
a

@[simp]
theorem add_commute.zero_left {M : Type u_1} [add_monoid M] (a : M) :
a

u (-u)

theorem commute.units_inv_right {M : Type u_1} [monoid M] {a : M} {u : units M} :
u u⁻¹

@[simp]
theorem commute.units_inv_right_iff {M : Type u_1} [monoid M] {a : M} {u : units M} :

@[simp]
(-u) u

theorem commute.units_inv_left {M : Type u_1} [monoid M] {u : units M} {a : M} :
a a

a a

@[simp]
theorem commute.units_inv_left_iff {M : Type u_1} [monoid M] {u : units M} {a : M} :
a a

@[simp]
a a

u₂ u₂

theorem commute.units_coe {M : Type u_1} [monoid M] {u₁ u₂ : units M} :
commute u₁ u₂commute u₁ u₂

u₂ u₂

theorem commute.units_of_coe {M : Type u_1} [monoid M] {u₁ u₂ : units M} :
commute u₁ u₂commute u₁ u₂

@[simp]
u₂ u₂

@[simp]
theorem commute.units_coe_iff {M : Type u_1} [monoid M] {u₁ u₂ : units M} :
commute u₁ u₂ commute u₁ u₂

theorem add_commute.neg_right {G : Type u_1} [add_group G] {a b : G} :
b (-b)

theorem commute.inv_right {G : Type u_1} [group G] {a b : G} :
b b⁻¹

@[simp]
theorem commute.inv_right_iff {G : Type u_1} [group G] {a b : G} :

@[simp]
theorem add_commute.neg_right_iff {G : Type u_1} [add_group G] {a b : G} :
(-b) b

theorem add_commute.neg_left {G : Type u_1} [add_group G] {a b : G} :

theorem commute.inv_left {G : Type u_1} [group G] {a b : G} :
b b

@[simp]
theorem commute.inv_left_iff {G : Type u_1} [group G] {a b : G} :
b b

@[simp]
theorem add_commute.neg_left_iff {G : Type u_1} [add_group G] {a b : G} :

theorem add_commute.neg_neg {G : Type u_1} [add_group G] {a b : G} :

theorem commute.inv_inv {G : Type u_1} [group G] {a b : G} :
b b⁻¹

@[simp]
theorem add_commute.neg_neg_iff {G : Type u_1} [add_group G] {a b : G} :

@[simp]
theorem commute.inv_inv_iff {G : Type u_1} [group G] {a b : G} :

b-a + b + a = b

theorem commute.inv_mul_cancel {G : Type u_1} [group G] {a b : G} :
b(a⁻¹ * b) * a = b

theorem commute.inv_mul_cancel_assoc {G : Type u_1} [group G] {a b : G} :
ba⁻¹ * b * a = b

b-a + (b + a) = b

theorem commute.mul_inv_cancel {G : Type u_1} [group G] {a b : G} :
b(a * b) * a⁻¹ = b

ba + b + -a = b

theorem commute.mul_inv_cancel_assoc {G : Type u_1} [group G] {a b : G} :
ba * b * a⁻¹ = b

ba + (b + -a) = b

@[simp]
theorem mul_inv_cancel_comm {G : Type u_1} [comm_group G] (a b : G) :
(a * b) * a⁻¹ = b

@[simp]
theorem add_neg_cancel_comm {G : Type u_1} (a b : G) :
a + b + -a = b

@[simp]
theorem mul_inv_cancel_comm_assoc {G : Type u_1} [comm_group G] (a b : G) :
a * b * a⁻¹ = b

@[simp]
theorem add_neg_cancel_comm_assoc {G : Type u_1} (a b : G) :
a + (b + -a) = b

@[simp]
theorem inv_mul_cancel_comm {G : Type u_1} [comm_group G] (a b : G) :
(a⁻¹ * b) * a = b

@[simp]
theorem neg_add_cancel_comm {G : Type u_1} (a b : G) :
-a + b + a = b

@[simp]
theorem neg_add_cancel_comm_assoc {G : Type u_1} (a b : G) :
-a + (b + a) = b

@[simp]
theorem inv_mul_cancel_comm_assoc {G : Type u_1} [comm_group G] (a b : G) :
a⁻¹ * b * a = b