# Documentation

Mathlib.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 SemiconjBy.

def AddCommute {S : Type u_1} [inst : Add S] (a : S) (b : S) :

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

Equations
def Commute {S : Type u_1} [inst : Mul S] (a : S) (b : S) :

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

Equations
theorem AddCommute.eq {S : Type u_1} [inst : Add S] {a : S} {b : S} (h : ) :
a + b = b + a

Equality behind add_commute a b; useful for rewriting.

theorem Commute.eq {S : Type u_1} [inst : Mul S] {a : S} {b : S} (h : Commute a b) :
a * b = b * a

Equality behind Commute a b; useful for rewriting.

@[simp]
theorem AddCommute.refl {S : Type u_1} [inst : Add S] (a : S) :

Any element commutes with itself.

@[simp]
theorem Commute.refl {S : Type u_1} [inst : Mul S] (a : S) :

Any element commutes with itself.

theorem AddCommute.symm {S : Type u_1} [inst : Add S] {a : S} {b : S} (h : ) :

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

theorem Commute.symm {S : Type u_1} [inst : Mul S] {a : S} {b : S} (h : Commute a b) :

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

theorem AddCommute.semiconjBy {S : Type u_1} [inst : Add S] {a : S} {b : S} (h : ) :
theorem Commute.semiconjBy {S : Type u_1} [inst : Mul S] {a : S} {b : S} (h : Commute a b) :
theorem AddCommute.symm_iff {S : Type u_1} [inst : Add S] {a : S} {b : S} :
theorem Commute.symm_iff {S : Type u_1} [inst : Mul S] {a : S} {b : S} :
Equations
Equations
instance Commute.instIsReflCommute {S : Type u_1} [inst : Mul S] :
IsRefl S Commute
Equations
instance AddCommute.on_isRefl {G : Type u_1} {S : Type u_2} [inst : Add S] {f : GS} :
IsRefl G fun a b => AddCommute (f a) (f b)
Equations
def AddCommute.on_isRefl.proof_1 {G : Type u_1} {S : Type u_2} [inst : Add S] {f : GS} :
IsRefl G fun a b => AddCommute (f a) (f b)
Equations
instance Commute.on_isRefl {G : Type u_1} {S : Type u_2} [inst : Mul S] {f : GS} :
IsRefl G fun a b => Commute (f a) (f b)
Equations
@[simp]
theorem AddCommute.add_right {S : Type u_1} [inst : ] {a : S} {b : S} {c : S} (hab : ) (hac : ) :

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

@[simp]
theorem Commute.mul_right {S : Type u_1} [inst : ] {a : S} {b : S} {c : S} (hab : Commute a b) (hac : Commute a c) :
Commute a (b * c)

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

@[simp]
theorem AddCommute.add_left {S : Type u_1} [inst : ] {a : S} {b : S} {c : S} (hac : ) (hbc : ) :

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

@[simp]
theorem Commute.mul_left {S : Type u_1} [inst : ] {a : S} {b : S} {c : S} (hac : Commute a c) (hbc : Commute b c) :
Commute (a * b) c

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

theorem AddCommute.right_comm {S : Type u_1} [inst : ] {b : S} {c : S} (h : ) (a : S) :
a + b + c = a + c + b
theorem Commute.right_comm {S : Type u_1} [inst : ] {b : S} {c : S} (h : Commute b c) (a : S) :
a * b * c = a * c * b
theorem AddCommute.left_comm {S : Type u_1} [inst : ] {a : S} {b : S} (h : ) (c : S) :
a + (b + c) = b + (a + c)
theorem Commute.left_comm {S : Type u_1} [inst : ] {a : S} {b : S} (h : Commute a b) (c : S) :
a * (b * c) = b * (a * c)
theorem AddCommute.add_add_add_comm {S : Type u_1} [inst : ] {b : S} {c : S} (hbc : ) (a : S) (d : S) :
a + b + (c + d) = a + c + (b + d)
theorem Commute.mul_mul_mul_comm {S : Type u_1} [inst : ] {b : S} {c : S} (hbc : Commute b c) (a : S) (d : S) :
a * b * (c * d) = a * c * (b * d)
theorem AddCommute.all {S : Type u_1} [inst : ] (a : S) (b : S) :
theorem Commute.all {S : Type u_1} [inst : ] (a : S) (b : S) :
@[simp]
theorem AddCommute.zero_right {M : Type u_1} [inst : ] (a : M) :
@[simp]
theorem Commute.one_right {M : Type u_1} [inst : ] (a : M) :
@[simp]
theorem AddCommute.zero_left {M : Type u_1} [inst : ] (a : M) :
@[simp]
theorem Commute.one_left {M : Type u_1} [inst : ] (a : M) :
@[simp]
theorem AddCommute.nsmul_right {M : Type u_1} [inst : ] {a : M} {b : M} (h : ) (n : ) :
@[simp]
theorem Commute.pow_right {M : Type u_1} [inst : ] {a : M} {b : M} (h : Commute a b) (n : ) :
Commute a (b ^ n)
@[simp]
theorem AddCommute.nsmul_left {M : Type u_1} [inst : ] {a : M} {b : M} (h : ) (n : ) :
@[simp]
theorem Commute.pow_left {M : Type u_1} [inst : ] {a : M} {b : M} (h : Commute a b) (n : ) :
Commute (a ^ n) b
@[simp]
theorem AddCommute.nsmul_nsmul {M : Type u_1} [inst : ] {a : M} {b : M} (h : ) (m : ) (n : ) :
@[simp]
theorem Commute.pow_pow {M : Type u_1} [inst : ] {a : M} {b : M} (h : Commute a b) (m : ) (n : ) :
Commute (a ^ m) (b ^ n)
theorem AddCommute.self_nsmul {M : Type u_1} [inst : ] (a : M) (n : ) :
theorem Commute.self_pow {M : Type u_1} [inst : ] (a : M) (n : ) :
Commute a (a ^ n)
theorem AddCommute.nsmul_self {M : Type u_1} [inst : ] (a : M) (n : ) :
theorem Commute.pow_self {M : Type u_1} [inst : ] (a : M) (n : ) :
Commute (a ^ n) a
theorem AddCommute.nsmul_nsmul_self {M : Type u_1} [inst : ] (a : M) (m : ) (n : ) :
theorem Commute.pow_pow_self {M : Type u_1} [inst : ] (a : M) (m : ) (n : ) :
Commute (a ^ m) (a ^ n)
theorem succ_nsmul' {M : Type u_1} [inst : ] (a : M) (n : ) :
(n + 1) a = n a + a
theorem pow_succ' {M : Type u_1} [inst : ] (a : M) (n : ) :
a ^ (n + 1) = a ^ n * a
theorem AddCommute.addUnits_neg_right {M : Type u_1} [inst : ] {a : M} {u : } :
theorem Commute.units_inv_right {M : Type u_1} [inst : ] {a : M} {u : Mˣ} :
Commute a uCommute a u⁻¹
@[simp]
theorem AddCommute.addUnits_neg_right_iff {M : Type u_1} [inst : ] {a : M} {u : } :
@[simp]
theorem Commute.units_inv_right_iff {M : Type u_1} [inst : ] {a : M} {u : Mˣ} :
Commute a u⁻¹ Commute a u
theorem AddCommute.addUnits_neg_left {M : Type u_1} [inst : ] {a : M} {u : } :
theorem Commute.units_inv_left {M : Type u_1} [inst : ] {a : M} {u : Mˣ} :
Commute (u) aCommute (u⁻¹) a
@[simp]
theorem AddCommute.addUnits_neg_left_iff {M : Type u_1} [inst : ] {a : M} {u : } :
@[simp]
theorem Commute.units_inv_left_iff {M : Type u_1} [inst : ] {a : M} {u : Mˣ} :
Commute (u⁻¹) a Commute (u) a
theorem AddCommute.addUnits_val {M : Type u_1} [inst : ] {u₁ : } {u₂ : } :
theorem Commute.units_val {M : Type u_1} [inst : ] {u₁ : Mˣ} {u₂ : Mˣ} :
Commute u₁ u₂Commute u₁ u₂
theorem AddCommute.addUnits_of_val {M : Type u_1} [inst : ] {u₁ : } {u₂ : } :
theorem Commute.units_of_val {M : Type u_1} [inst : ] {u₁ : Mˣ} {u₂ : Mˣ} :
Commute u₁ u₂Commute u₁ u₂
@[simp]
theorem AddCommute.addUnits_val_iff {M : Type u_1} [inst : ] {u₁ : } {u₂ : } :
@[simp]
theorem Commute.units_val_iff {M : Type u_1} [inst : ] {u₁ : Mˣ} {u₂ : Mˣ} :
Commute u₁ u₂ Commute u₁ u₂
def AddUnits.leftOfAdd.proof_2 {M : Type u_1} [inst : ] (u : ) (a : M) (b : M) (hu : a + b = u) (hc : ) :
b + ↑(-u) + a = 0
Equations
• (_ : b + ↑(-u) + a = 0) = (_ : b + ↑(-u) + a = 0)
def AddUnits.leftOfAdd.proof_1 {M : Type u_1} [inst : ] (u : ) (a : M) (b : M) (hu : a + b = u) :
a + (b + ↑(-u)) = 0
Equations
• (_ : a + (b + ↑(-u)) = 0) = (_ : a + (b + ↑(-u)) = 0)
def AddUnits.leftOfAdd {M : Type u_1} [inst : ] (u : ) (a : M) (b : M) (hu : a + b = u) (hc : ) :

If the sum of two commuting elements is an additive unit, then the left summand is an additive unit.

Equations
def Units.leftOfMul {M : Type u_1} [inst : ] (u : Mˣ) (a : M) (b : M) (hu : a * b = u) (hc : Commute a b) :

If the product of two commuting elements is a unit, then the left multiplier is a unit.

Equations
def AddUnits.rightOfAdd.proof_1 {M : Type u_1} [inst : ] (u : ) (a : M) (b : M) (hu : a + b = u) (hc : ) :
b + a = u
Equations
• (_ : b + a = u) = (_ : b + a = u)
def AddUnits.rightOfAdd.proof_2 {M : Type u_1} [inst : ] (a : M) (b : M) (hc : ) :
Equations
• (_ : ) = (_ : )
def AddUnits.rightOfAdd {M : Type u_1} [inst : ] (u : ) (a : M) (b : M) (hu : a + b = u) (hc : ) :

If the sum of two commuting elements is an additive unit, then the right summand is an additive unit.

Equations
def Units.rightOfMul {M : Type u_1} [inst : ] (u : Mˣ) (a : M) (b : M) (hu : a * b = u) (hc : Commute a b) :

If the product of two commuting elements is a unit, then the right multiplier is a unit.

Equations
theorem AddCommute.isAddUnit_add_iff {M : Type u_1} [inst : ] {a : M} {b : M} (h : ) :
(x : IsAddUnit (a + b)) → ((u : ) → (hu : u = a + b) → motive (_ : u, u = a + b)) → motive x
Equations
theorem Commute.isUnit_mul_iff {M : Type u_1} [inst : ] {a : M} {b : M} (h : Commute a b) :
IsUnit (a * b)
@[simp]
theorem isAddUnit_add_self_iff {M : Type u_1} [inst : ] {a : M} :
@[simp]
theorem isUnit_mul_self_iff {M : Type u_1} [inst : ] {a : M} :
IsUnit (a * a)
theorem AddCommute.neg_neg {G : Type u_1} [inst : ] {a : G} {b : G} :
theorem Commute.inv_inv {G : Type u_1} [inst : ] {a : G} {b : G} :
Commute a b
@[simp]
theorem AddCommute.neg_neg_iff {G : Type u_1} [inst : ] {a : G} {b : G} :
@[simp]
theorem Commute.inv_inv_iff {G : Type u_1} [inst : ] {a : G} {b : G} :
theorem AddCommute.add_neg {G : Type u_1} [inst : ] {a : G} {b : G} (hab : ) :
-(a + b) = -a + -b
theorem Commute.mul_inv {G : Type u_1} [inst : ] {a : G} {b : G} (hab : Commute a b) :
(a * b)⁻¹ = a⁻¹ * b⁻¹
theorem AddCommute.neg {G : Type u_1} [inst : ] {a : G} {b : G} (hab : ) :
-(a + b) = -a + -b
theorem Commute.inv {G : Type u_1} [inst : ] {a : G} {b : G} (hab : Commute a b) :
(a * b)⁻¹ = a⁻¹ * b⁻¹
theorem AddCommute.sub_add_sub_comm {G : Type u_1} [inst : ] {a : G} {b : G} {c : G} {d : G} (hbd : ) (hbc : AddCommute (-b) c) :
a - b + (c - d) = a + c - (b + d)
theorem Commute.div_mul_div_comm {G : Type u_1} [inst : ] {a : G} {b : G} {c : G} {d : G} (hbd : Commute b d) (hbc : ) :
a / b * (c / d) = a * c / (b * d)
theorem AddCommute.add_sub_add_comm {G : Type u_1} [inst : ] {a : G} {b : G} {c : G} {d : G} (hcd : ) (hbc : AddCommute b (-c)) :
a + b - (c + d) = a - c + (b - d)
theorem Commute.mul_div_mul_comm {G : Type u_1} [inst : ] {a : G} {b : G} {c : G} {d : G} (hcd : Commute c d) (hbc : ) :
a * b / (c * d) = a / c * (b / d)
theorem AddCommute.sub_sub_sub_comm {G : Type u_1} [inst : ] {a : G} {b : G} {c : G} {d : G} (hbc : ) (hbd : AddCommute (-b) d) (hcd : AddCommute (-c) d) :
a - b - (c - d) = a - c - (b - d)
theorem Commute.div_div_div_comm {G : Type u_1} [inst : ] {a : G} {b : G} {c : G} {d : G} (hbc : Commute b c) (hbd : ) (hcd : ) :
a / b / (c / d) = a / c / (b / d)
theorem AddCommute.neg_right {G : Type u_1} [inst : ] {a : G} {b : G} :
theorem Commute.inv_right {G : Type u_1} [inst : ] {a : G} {b : G} :
Commute a b
@[simp]
theorem AddCommute.neg_right_iff {G : Type u_1} [inst : ] {a : G} {b : G} :
@[simp]
theorem Commute.inv_right_iff {G : Type u_1} [inst : ] {a : G} {b : G} :
theorem AddCommute.neg_left {G : Type u_1} [inst : ] {a : G} {b : G} :
theorem Commute.inv_left {G : Type u_1} [inst : ] {a : G} {b : G} :
Commute a b
@[simp]
theorem AddCommute.neg_left_iff {G : Type u_1} [inst : ] {a : G} {b : G} :
@[simp]
theorem Commute.inv_left_iff {G : Type u_1} [inst : ] {a : G} {b : G} :
theorem AddCommute.neg_add_cancel {G : Type u_1} [inst : ] {a : G} {b : G} (h : ) :
-a + b + a = b
theorem Commute.inv_mul_cancel {G : Type u_1} [inst : ] {a : G} {b : G} (h : Commute a b) :
a⁻¹ * b * a = b
theorem AddCommute.neg_add_cancel_assoc {G : Type u_1} [inst : ] {a : G} {b : G} (h : ) :
-a + (b + a) = b
theorem Commute.inv_mul_cancel_assoc {G : Type u_1} [inst : ] {a : G} {b : G} (h : Commute a b) :
a⁻¹ * (b * a) = b
theorem AddCommute.add_neg_cancel {G : Type u_1} [inst : ] {a : G} {b : G} (h : ) :
a + b + -a = b
theorem Commute.mul_inv_cancel {G : Type u_1} [inst : ] {a : G} {b : G} (h : Commute a b) :
a * b * a⁻¹ = b
theorem AddCommute.add_neg_cancel_assoc {G : Type u_1} [inst : ] {a : G} {b : G} (h : ) :
a + (b + -a) = b
theorem Commute.mul_inv_cancel_assoc {G : Type u_1} [inst : ] {a : G} {b : G} (h : Commute a b) :
a * (b * a⁻¹) = b
@[simp]
theorem add_neg_cancel_comm {G : Type u_1} [inst : ] (a : G) (b : G) :
a + b + -a = b
@[simp]
theorem mul_inv_cancel_comm {G : Type u_1} [inst : ] (a : G) (b : G) :
a * b * a⁻¹ = b
@[simp]
theorem add_neg_cancel_comm_assoc {G : Type u_1} [inst : ] (a : G) (b : G) :
a + (b + -a) = b
@[simp]
theorem mul_inv_cancel_comm_assoc {G : Type u_1} [inst : ] (a : G) (b : G) :
a * (b * a⁻¹) = b
@[simp]
theorem neg_add_cancel_comm {G : Type u_1} [inst : ] (a : G) (b : G) :
-a + b + a = b
@[simp]
theorem inv_mul_cancel_comm {G : Type u_1} [inst : ] (a : G) (b : G) :
a⁻¹ * b * a = b
@[simp]
theorem neg_add_cancel_comm_assoc {G : Type u_1} [inst : ] (a : G) (b : G) :
-a + (b + a) = b
@[simp]
theorem inv_mul_cancel_comm_assoc {G : Type u_1} [inst : ] (a : G) (b : G) :
a⁻¹ * (b * a) = b