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_2} [Add S] (a : S) (b : S) : Prop

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

Equations

• AddCommute a b = AddSemiconjBy a b b

def Commute {S : Type u_2} [Mul S] (a : S) (b : S) : Prop

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

Equations

• Commute a b = SemiconjBy a b b

theorem addCommute_iff_eq {S : Type u_2} [Add S] (a : S) (b : S) : AddCommute a b ↔ a + b = b + a

theorem commute_iff_eq {S : Type u_2} [Mul S] (a : S) (b : S) : Commute a b ↔ a * b = b * a

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

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

Equality behind AddCommute a b; useful for rewriting.

theorem Commute.eq {S : Type u_2} [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_2} [Add S] (a : S) : AddCommute a a

Any element commutes with itself.

@[simp]

theorem Commute.refl {S : Type u_2} [Mul S] (a : S) : Commute a a

Any element commutes with itself.

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

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

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

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

theorem AddCommute.addSemiconjBy {S : Type u_2} [Add S] {a : S} {b : S} (h : AddCommute a b) : AddSemiconjBy a b b

theorem Commute.semiconjBy {S : Type u_2} [Mul S] {a : S} {b : S} (h : Commute a b) : SemiconjBy a b b

theorem AddCommute.symm_iff {S : Type u_2} [Add S] {a : S} {b : S} : AddCommute a b ↔ AddCommute b a

theorem Commute.symm_iff {S : Type u_2} [Mul S] {a : S} {b : S} : Commute a b ↔ Commute b a

instance AddCommute.instIsReflAddCommute {S : Type u_2} [Add S] : IsRefl S AddCommute

Equations

• ⋯ = ⋯

instance Commute.instIsReflCommute {S : Type u_2} [Mul S] : IsRefl S Commute

Equations

• ⋯ = ⋯

instance AddCommute.on_isRefl {G : Type u_1} {S : Type u_2} [Add S] {f : G → S} : IsRefl G fun (a b : G) => AddCommute (f a) (f b)

Equations

• ⋯ = ⋯

instance Commute.on_isRefl {G : Type u_1} {S : Type u_2} [Mul S] {f : G → S} : IsRefl G fun (a b : G) => Commute (f a) (f b)

Equations

• ⋯ = ⋯

@[simp]

theorem AddCommute.add_right {S : Type u_2} [AddSemigroup S] {a : S} {b : S} {c : S} (hab : AddCommute a b) (hac : AddCommute a c) : AddCommute a (b + c)

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

@[simp]

theorem Commute.mul_right {S : Type u_2} [Semigroup S] {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_2} [AddSemigroup S] {a : S} {b : S} {c : S} (hac : AddCommute a c) (hbc : AddCommute b c) : AddCommute (a + b) c

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

@[simp]

theorem Commute.mul_left {S : Type u_2} [Semigroup S] {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_2} [AddSemigroup S] {b : S} {c : S} (h : AddCommute b c) (a : S) : a + b + c = a + c + b

theorem Commute.right_comm {S : Type u_2} [Semigroup S] {b : S} {c : S} (h : Commute b c) (a : S) : a * b * c = a * c * b

theorem AddCommute.left_comm {S : Type u_2} [AddSemigroup S] {a : S} {b : S} (h : AddCommute a b) (c : S) : a + (b + c) = b + (a + c)

theorem Commute.left_comm {S : Type u_2} [Semigroup S] {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_2} [AddSemigroup S] {b : S} {c : S} (hbc : AddCommute b c) (a : S) (d : S) : a + b + (c + d) = a + c + (b + d)

theorem Commute.mul_mul_mul_comm {S : Type u_2} [Semigroup S] {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_2} [AddCommMagma S] (a : S) (b : S) : AddCommute a b

theorem Commute.all {S : Type u_2} [CommMagma S] (a : S) (b : S) : Commute a b

@[simp]

theorem AddCommute.zero_right {M : Type u_2} [AddZeroClass M] (a : M) : AddCommute a 0

@[simp]

theorem Commute.one_right {M : Type u_2} [MulOneClass M] (a : M) : Commute a 1

@[simp]

theorem AddCommute.zero_left {M : Type u_2} [AddZeroClass M] (a : M) : AddCommute 0 a

@[simp]

theorem Commute.one_left {M : Type u_2} [MulOneClass M] (a : M) : Commute 1 a

@[simp]

theorem AddCommute.nsmul_right {M : Type u_2} [AddMonoid M] {a : M} {b : M} (h : AddCommute a b) (n : ℕ) : AddCommute a (n • b)

@[simp]

theorem Commute.pow_right {M : Type u_2} [Monoid M] {a : M} {b : M} (h : Commute a b) (n : ℕ) : Commute a (b ^ n)

@[simp]

theorem AddCommute.nsmul_left {M : Type u_2} [AddMonoid M] {a : M} {b : M} (h : AddCommute a b) (n : ℕ) : AddCommute (n • a) b

@[simp]

theorem Commute.pow_left {M : Type u_2} [Monoid M] {a : M} {b : M} (h : Commute a b) (n : ℕ) : Commute (a ^ n) b

@[simp]

theorem AddCommute.nsmul_nsmul {M : Type u_2} [AddMonoid M] {a : M} {b : M} (h : AddCommute a b) (m : ℕ) (n : ℕ) : AddCommute (m • a) (n • b)

@[simp]

theorem Commute.pow_pow {M : Type u_2} [Monoid M] {a : M} {b : M} (h : Commute a b) (m : ℕ) (n : ℕ) : Commute (a ^ m) (b ^ n)

theorem AddCommute.self_nsmul {M : Type u_2} [AddMonoid M] (a : M) (n : ℕ) : AddCommute a (n • a)

theorem Commute.self_pow {M : Type u_2} [Monoid M] (a : M) (n : ℕ) : Commute a (a ^ n)

theorem AddCommute.nsmul_self {M : Type u_2} [AddMonoid M] (a : M) (n : ℕ) : AddCommute (n • a) a

theorem Commute.pow_self {M : Type u_2} [Monoid M] (a : M) (n : ℕ) : Commute (a ^ n) a

theorem AddCommute.nsmul_nsmul_self {M : Type u_2} [AddMonoid M] (a : M) (m : ℕ) (n : ℕ) : AddCommute (m • a) (n • a)

theorem Commute.pow_pow_self {M : Type u_2} [Monoid M] (a : M) (m : ℕ) (n : ℕ) : Commute (a ^ m) (a ^ n)

theorem AddCommute.add_neg {G : Type u_1} [SubtractionMonoid G] {a : G} {b : G} (hab : AddCommute a b) : -(a + b) = -a + -b

theorem Commute.mul_inv {G : Type u_1} [DivisionMonoid G] {a : G} {b : G} (hab : Commute a b) : (a * b)⁻¹ = a⁻¹ * b⁻¹

theorem AddCommute.neg {G : Type u_1} [SubtractionMonoid G] {a : G} {b : G} (hab : AddCommute a b) : -(a + b) = -a + -b

theorem Commute.inv {G : Type u_1} [DivisionMonoid G] {a : G} {b : G} (hab : Commute a b) : (a * b)⁻¹ = a⁻¹ * b⁻¹

theorem AddCommute.add_neg_cancel {G : Type u_1} [AddGroup G] {a : G} {b : G} (h : AddCommute a b) : a + b + -a = b

theorem Commute.mul_inv_cancel {G : Type u_1} [Group G] {a : G} {b : G} (h : Commute a b) : a * b * a⁻¹ = b

theorem AddCommute.add_neg_cancel_assoc {G : Type u_1} [AddGroup G] {a : G} {b : G} (h : AddCommute a b) : a + (b + -a) = b

theorem Commute.mul_inv_cancel_assoc {G : Type u_1} [Group G] {a : G} {b : G} (h : Commute a b) : a * (b * a⁻¹) = b

theorem succ_nsmul' {M : Type u_2} [AddMonoid M] (a : M) (n : ℕ) : (n + 1) • a = a + n • a

theorem pow_succ' {M : Type u_2} [Monoid M] (a : M) (n : ℕ) : a ^ (n + 1) = a * a ^ n

theorem add_nsmul_sub_zero {M : Type u_2} [AddMonoid M] {n : ℕ} (hn : n ≠ 0) (a : M) : a + (n - 1) • a = n • a

theorem mul_pow_sub_one {M : Type u_2} [Monoid M] {n : ℕ} (hn : n ≠ 0) (a : M) : a * a ^ (n - 1) = a ^ n

theorem nsmul_sub_zero_add {M : Type u_2} [AddMonoid M] {n : ℕ} (hn : n ≠ 0) (a : M) : (n - 1) • a + a = n • a

theorem pow_sub_one_mul {M : Type u_2} [Monoid M] {n : ℕ} (hn : n ≠ 0) (a : M) : a ^ (n - 1) * a = a ^ n

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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