mathlib3 documentation

algebra.group.commute

Commuting pairs of elements in monoids #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

def add_commute {S : Type u_1} [has_add S] (a b : S) :

Prop

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

Equations

add_commute a b = add_semiconj_by a b b

Instances for add_commute

def commute {S : Type u_1} [has_mul S] (a b : S) :

Prop

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

Equations

commute a b = semiconj_by a b b

Instances for commute

@[protected]

theorem commute.eq {S : Type u_2} [has_mul S] {a b : S} (h : commute a b) :

a * b = b * a

Equality behind commute a b; useful for rewriting.

@[protected]

theorem add_commute.eq {S : Type u_2} [has_add S] {a b : S} (h : add_commute a b) :

a + b = b + a

Equality behind add_commute a b; useful for rewriting.

@[protected, simp, refl]

theorem add_commute.refl {S : Type u_2} [has_add S] (a : S) :

add_commute a a

Any element commutes with itself.

@[protected, simp, refl]

theorem commute.refl {S : Type u_2} [has_mul S] (a : S) :

Any element commutes with itself.

@[protected, symm]

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

add_commute b a

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

@[protected, symm]

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

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

@[protected]

theorem commute.semiconj_by {S : Type u_2} [has_mul S] {a b : S} (h : commute a b) :

semiconj_by a b b

@[protected]

theorem add_commute.semiconj_by {S : Type u_2} [has_add S] {a b : S} (h : add_commute a b) :

add_semiconj_by a b b

@[protected]

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

add_commute a b ↔ add_commute b a

@[protected]

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

commute a b ↔ commute b a

@[protected, instance]

def commute.is_refl {S : Type u_2} [has_mul S] :

is_refl S commute

@[protected, instance]

def add_commute.is_refl {S : Type u_2} [has_add S] :

is_refl S add_commute

@[protected, instance]

def commute.on_is_refl {G : Type u_1} {S : Type u_2} [has_mul S] {f : G → S} :

is_refl G (λ (a b : G), commute (f a) (f b))

@[protected, instance]

def add_commute.on_is_refl {G : Type u_1} {S : Type u_2} [has_add S] {f : G → S} :

is_refl G (λ (a b : G), add_commute (f a) (f b))

@[simp]

theorem commute.mul_right {S : Type u_2} [semigroup S] {a b 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 add_commute.add_right {S : Type u_2} [add_semigroup S] {a b c : S} (hab : add_commute a b) (hac : add_commute a c) :

add_commute a (b + c)

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

@[simp]

theorem commute.mul_left {S : Type u_2} [semigroup S] {a b 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.

@[simp]

theorem add_commute.add_left {S : Type u_2} [add_semigroup S] {a b c : S} (hac : add_commute a c) (hbc : add_commute b c) :

add_commute (a + b) c

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

@[protected]

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

a * b * c = a * c * b

@[protected]

theorem add_commute.right_comm {S : Type u_2} [add_semigroup S] {b c : S} (h : add_commute b c) (a : S) :

a + b + c = a + c + b

@[protected]

theorem add_commute.left_comm {S : Type u_2} [add_semigroup S] {a b : S} (h : add_commute a b) (c : S) :

a + (b + c) = b + (a + c)

@[protected]

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

a * (b * c) = b * (a * c)

@[protected]

theorem add_commute.add_add_add_comm {S : Type u_2} [add_semigroup S] {b c : S} (hbc : add_commute b c) (a d : S) :

a + b + (c + d) = a + c + (b + d)

@[protected]

theorem commute.mul_mul_mul_comm {S : Type u_2} [semigroup S] {b c : S} (hbc : commute b c) (a d : S) :

a * b * (c * d) = a * c * (b * d)

@[protected]

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

@[protected]

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

add_commute a b

@[simp]

theorem commute.one_right {M : Type u_2} [mul_one_class M] (a : M) :

@[simp]

theorem add_commute.zero_right {M : Type u_2} [add_zero_class M] (a : M) :

add_commute a 0

@[simp]

theorem commute.one_left {M : Type u_2} [mul_one_class M] (a : M) :

@[simp]

theorem add_commute.zero_left {M : Type u_2} [add_zero_class M] (a : M) :

add_commute 0 a

@[simp]

theorem add_commute.nsmul_right {M : Type u_2} [add_monoid M] {a b : M} (h : add_commute a b) (n : ℕ) :

add_commute a (n • b)

@[simp]

theorem commute.pow_right {M : Type u_2} [monoid M] {a b : M} (h : commute a b) (n : ℕ) :

commute a (b ^ n)

@[simp]

theorem commute.pow_left {M : Type u_2} [monoid M] {a b : M} (h : commute a b) (n : ℕ) :

commute (a ^ n) b

@[simp]

theorem add_commute.nsmul_left {M : Type u_2} [add_monoid M] {a b : M} (h : add_commute a b) (n : ℕ) :

add_commute (n • a) b

@[simp]

theorem add_commute.nsmul_nsmul {M : Type u_2} [add_monoid M] {a b : M} (h : add_commute a b) (m n : ℕ) :

add_commute (m • a) (n • b)

@[simp]

theorem commute.pow_pow {M : Type u_2} [monoid M] {a b : M} (h : commute a b) (m n : ℕ) :

commute (a ^ m) (b ^ n)

@[simp]

theorem commute.self_pow {M : Type u_2} [monoid M] (a : M) (n : ℕ) :

commute a (a ^ n)

@[simp]

theorem add_commute.self_nsmul {M : Type u_2} [add_monoid M] (a : M) (n : ℕ) :

add_commute a (n • a)

@[simp]

theorem commute.pow_self {M : Type u_2} [monoid M] (a : M) (n : ℕ) :

commute (a ^ n) a

@[simp]

theorem add_commute.nsmul_self {M : Type u_2} [add_monoid M] (a : M) (n : ℕ) :

add_commute (n • a) a

@[simp]

theorem add_commute.nsmul_nsmul_self {M : Type u_2} [add_monoid M] (a : M) (m n : ℕ) :

add_commute (m • a) (n • a)

@[simp]

theorem commute.pow_pow_self {M : Type u_2} [monoid M] (a : M) (m n : ℕ) :

commute (a ^ m) (a ^ n)

theorem pow_succ' {M : Type u_2} [monoid M] (a : M) (n : ℕ) :

a ^ (n + 1) = a ^ n * a

theorem succ_nsmul' {M : Type u_2} [add_monoid M] (a : M) (n : ℕ) :

(n + 1) • a = n • a + a

theorem add_commute.add_units_neg_right {M : Type u_2} [add_monoid M] {a : M} {u : add_units M} :

add_commute a ↑u → add_commute a (↑-u)

theorem commute.units_inv_right {M : Type u_2} [monoid M] {a : M} {u : Mˣ} :

commute a ↑u → commute a ↑u⁻¹

@[simp]

theorem add_commute.add_units_neg_right_iff {M : Type u_2} [add_monoid M] {a : M} {u : add_units M} :

add_commute a (↑-u) ↔ add_commute a ↑u

@[simp]

theorem commute.units_inv_right_iff {M : Type u_2} [monoid M] {a : M} {u : Mˣ} :

commute a ↑u⁻¹ ↔ commute a ↑u

theorem commute.units_inv_left {M : Type u_2} [monoid M] {a : M} {u : Mˣ} :

commute ↑u a → commute ↑u⁻¹ a

theorem add_commute.add_units_neg_left {M : Type u_2} [add_monoid M] {a : M} {u : add_units M} :

add_commute ↑u a → add_commute (↑-u) a

@[simp]

theorem add_commute.add_units_neg_left_iff {M : Type u_2} [add_monoid M] {a : M} {u : add_units M} :

add_commute (↑-u) a ↔ add_commute ↑u a

@[simp]

theorem commute.units_inv_left_iff {M : Type u_2} [monoid M] {a : M} {u : Mˣ} :

commute ↑u⁻¹ a ↔ commute ↑u a

theorem add_commute.add_units_coe {M : Type u_2} [add_monoid M] {u₁ u₂ : add_units M} :

add_commute u₁ u₂ → add_commute ↑u₁ ↑u₂

theorem commute.units_coe {M : Type u_2} [monoid M] {u₁ u₂ : Mˣ} :

commute u₁ u₂ → commute ↑u₁ ↑u₂

theorem add_commute.add_units_of_coe {M : Type u_2} [add_monoid M] {u₁ u₂ : add_units M} :

add_commute ↑u₁ ↑u₂ → add_commute u₁ u₂

theorem commute.units_of_coe {M : Type u_2} [monoid M] {u₁ u₂ : Mˣ} :

commute ↑u₁ ↑u₂ → commute u₁ u₂

@[simp]

theorem commute.units_coe_iff {M : Type u_2} [monoid M] {u₁ u₂ : Mˣ} :

commute ↑u₁ ↑u₂ ↔ commute u₁ u₂

@[simp]

theorem add_commute.add_units_coe_iff {M : Type u_2} [add_monoid M] {u₁ u₂ : add_units M} :

add_commute ↑u₁ ↑u₂ ↔ add_commute u₁ u₂

def units.left_of_mul {M : Type u_2} [monoid M] (u : Mˣ) (a 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

u.left_of_mul a b hu hc = {val := a, inv := b * ↑u⁻¹, val_inv := _, inv_val := _}

def add_units.left_of_add {M : Type u_2} [add_monoid M] (u : add_units M) (a b : M) (hu : a + b = ↑u) (hc : add_commute a b) :

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

Equations

u.left_of_add a b hu hc = {val := a, neg := b + ↑-u, val_neg := _, neg_val := _}

def add_units.right_of_add {M : Type u_2} [add_monoid M] (u : add_units M) (a b : M) (hu : a + b = ↑u) (hc : add_commute a b) :

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

Equations

u.right_of_add a b hu hc = u.left_of_add b a _ _

def units.right_of_mul {M : Type u_2} [monoid M] (u : Mˣ) (a 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

u.right_of_mul a b hu hc = u.left_of_mul b a _ _

theorem add_commute.is_add_unit_add_iff {M : Type u_2} [add_monoid M] {a b : M} (h : add_commute a b) :

is_add_unit (a + b) ↔ is_add_unit a ∧ is_add_unit b

theorem commute.is_unit_mul_iff {M : Type u_2} [monoid M] {a b : M} (h : commute a b) :

is_unit (a * b) ↔ is_unit a ∧ is_unit b

@[simp]

theorem is_add_unit_add_self_iff {M : Type u_2} [add_monoid M] {a : M} :

is_add_unit (a + a) ↔ is_add_unit a

@[simp]

theorem is_unit_mul_self_iff {M : Type u_2} [monoid M] {a : M} :

is_unit (a * a) ↔ is_unit a

@[protected]

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

add_commute a b → add_commute (-a) (-b)

@[protected]

theorem commute.inv_inv {G : Type u_1} [division_monoid G] {a b : G} :

commute a b → commute a⁻¹ b⁻¹

@[simp]

theorem add_commute.neg_neg_iff {G : Type u_1} [subtraction_monoid G] {a b : G} :

add_commute (-a) (-b) ↔ add_commute a b

@[simp]

theorem commute.inv_inv_iff {G : Type u_1} [division_monoid G] {a b : G} :

commute a⁻¹ b⁻¹ ↔ commute a b

@[protected]

theorem add_commute.add_neg {G : Type u_1} [subtraction_monoid G] {a b : G} (hab : add_commute a b) :

-(a + b) = -a + -b

@[protected]

theorem commute.mul_inv {G : Type u_1} [division_monoid G] {a b : G} (hab : commute a b) :

(a * b)⁻¹ = a⁻¹ * b⁻¹

@[protected]

theorem add_commute.neg {G : Type u_1} [subtraction_monoid G] {a b : G} (hab : add_commute a b) :

-(a + b) = -a + -b

@[protected]

theorem commute.inv {G : Type u_1} [division_monoid G] {a b : G} (hab : commute a b) :

(a * b)⁻¹ = a⁻¹ * b⁻¹

@[protected]

theorem add_commute.sub_add_sub_comm {G : Type u_1} [subtraction_monoid G] {a b c d : G} (hbd : add_commute b d) (hbc : add_commute (-b) c) :

a - b + (c - d) = a + c - (b + d)

@[protected]

theorem commute.div_mul_div_comm {G : Type u_1} [division_monoid G] {a b c d : G} (hbd : commute b d) (hbc : commute b⁻¹ c) :

a / b * (c / d) = a * c / (b * d)

@[protected]

theorem add_commute.add_sub_add_comm {G : Type u_1} [subtraction_monoid G] {a b c d : G} (hcd : add_commute c d) (hbc : add_commute b (-c)) :

a + b - (c + d) = a - c + (b - d)

@[protected]

theorem commute.mul_div_mul_comm {G : Type u_1} [division_monoid G] {a b c d : G} (hcd : commute c d) (hbc : commute b c⁻¹) :

a * b / (c * d) = a / c * (b / d)

@[protected]

theorem add_commute.sub_sub_sub_comm {G : Type u_1} [subtraction_monoid G] {a b c d : G} (hbc : add_commute b c) (hbd : add_commute (-b) d) (hcd : add_commute (-c) d) :

a - b - (c - d) = a - c - (b - d)

@[protected]

theorem commute.div_div_div_comm {G : Type u_1} [division_monoid G] {a b c d : G} (hbc : commute b c) (hbd : commute b⁻¹ d) (hcd : commute c⁻¹ d) :

a / b / (c / d) = a / c / (b / d)

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

add_commute a b → add_commute a (-b)

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

commute a b → commute a b⁻¹

@[simp]

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

commute a b⁻¹ ↔ commute a b

@[simp]

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

add_commute a (-b) ↔ add_commute a b

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

add_commute a b → add_commute (-a) b

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

commute a b → commute a⁻¹ b

@[simp]

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

commute a⁻¹ b ↔ commute a b

@[simp]

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

add_commute (-a) b ↔ add_commute a b

@[protected]

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

-a + b + a = b

@[protected]

theorem commute.inv_mul_cancel {G : Type u_1} [group G] {a b : G} (h : commute a b) :

a⁻¹ * b * a = b

theorem commute.inv_mul_cancel_assoc {G : Type u_1} [group G] {a b : G} (h : commute a b) :

a⁻¹ * (b * a) = b

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

-a + (b + a) = b

@[protected]

theorem commute.mul_inv_cancel {G : Type u_1} [group G] {a b : G} (h : commute a b) :

a * b * a⁻¹ = b

@[protected]

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

a + b + -a = b

theorem commute.mul_inv_cancel_assoc {G : Type u_1} [group G] {a b : G} (h : commute a b) :

a * (b * a⁻¹) = b

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

a + (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} [add_comm_group G] (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} [add_comm_group G] (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} [add_comm_group G] (a b : G) :

-a + b + a = b

@[simp]

theorem neg_add_cancel_comm_assoc {G : Type u_1} [add_comm_group G] (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