Documentation

Mathlib.Algebra.Group.Commute.Defs

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.

source
def AddCommute {S : Type u_2} [Add S] (a : S) (b : S) :
Prop

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

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

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

    Equations
    Instances For
      source
      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.

      source
      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.

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

      Any element commutes with itself.

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

      Any element commutes with itself.

      source
      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.

      source
      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.

      source
      theorem AddCommute.addSemiconjBy {S : Type u_2} [Add S] {a : S} {b : S} (h : AddCommute a b) :
      AddSemiconjBy a b b
      source
      theorem Commute.semiconjBy {S : Type u_2} [Mul S] {a : S} {b : S} (h : Commute a b) :
      SemiconjBy a b b
      source
      theorem AddCommute.symm_iff {S : Type u_2} [Add S] {a : S} {b : S} :
      AddCommute a b ↔ AddCommute b a
      source
      theorem Commute.symm_iff {S : Type u_2} [Mul S] {a : S} {b : S} :
      Commute a b ↔ Commute b a
      source
      instance AddCommute.instIsReflAddCommute {S : Type u_2} [Add S] :
      IsRefl S AddCommute
      Equations
      source
      instance Commute.instIsReflCommute {S : Type u_2} [Mul S] :
      IsRefl S Commute
      Equations
      source
      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
      source
      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
      source
      @[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.

      source
      @[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.

      source
      @[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.

      source
      @[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.

      source
      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
      source
      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
      source
      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)
      source
      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)
      source
      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)
      source
      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)
      source
      theorem AddCommute.all {S : Type u_2} [AddCommMagma S] (a : S) (b : S) :
      AddCommute a b
      source
      theorem Commute.all {S : Type u_2} [CommMagma S] (a : S) (b : S) :
      Commute a b
      source
      @[simp]
      theorem AddCommute.zero_right {M : Type u_2} [AddZeroClass M] (a : M) :
      AddCommute a 0
      source
      @[simp]
      theorem Commute.one_right {M : Type u_2} [MulOneClass M] (a : M) :
      Commute a 1
      source
      @[simp]
      theorem AddCommute.zero_left {M : Type u_2} [AddZeroClass M] (a : M) :
      AddCommute 0 a
      source
      @[simp]
      theorem Commute.one_left {M : Type u_2} [MulOneClass M] (a : M) :
      Commute 1 a
      source
      @[simp]
      theorem AddCommute.nsmul_right {M : Type u_2} [AddMonoid M] {a : M} {b : M} (h : AddCommute a b) (n : ℕ) :
      AddCommute a (n • b)
      source
      @[simp]
      theorem Commute.pow_right {M : Type u_2} [Monoid M] {a : M} {b : M} (h : Commute a b) (n : ℕ) :
      Commute a (b ^ n)
      source
      @[simp]
      theorem AddCommute.nsmul_left {M : Type u_2} [AddMonoid M] {a : M} {b : M} (h : AddCommute a b) (n : ℕ) :
      AddCommute (n • a) b
      source
      @[simp]
      theorem Commute.pow_left {M : Type u_2} [Monoid M] {a : M} {b : M} (h : Commute a b) (n : ℕ) :
      Commute (a ^ n) b
      source
      @[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)
      source
      @[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)
      source
      theorem AddCommute.self_nsmul {M : Type u_2} [AddMonoid M] (a : M) (n : ℕ) :
      AddCommute a (n • a)
      source
      theorem Commute.self_pow {M : Type u_2} [Monoid M] (a : M) (n : ℕ) :
      Commute a (a ^ n)
      source
      theorem AddCommute.nsmul_self {M : Type u_2} [AddMonoid M] (a : M) (n : ℕ) :
      AddCommute (n • a) a
      source
      theorem Commute.pow_self {M : Type u_2} [Monoid M] (a : M) (n : ℕ) :
      Commute (a ^ n) a
      source
      theorem AddCommute.nsmul_nsmul_self {M : Type u_2} [AddMonoid M] (a : M) (m : ℕ) (n : ℕ) :
      AddCommute (m • a) (n • a)
      source
      theorem Commute.pow_pow_self {M : Type u_2} [Monoid M] (a : M) (m : ℕ) (n : ℕ) :
      Commute (a ^ m) (a ^ n)
      source
      theorem AddCommute.add_neg {G : Type u_1} [SubtractionMonoid G] {a : G} {b : G} (hab : AddCommute a b) :
      -(a + b) = -a + -b
      source
      theorem Commute.mul_inv {G : Type u_1} [DivisionMonoid G] {a : G} {b : G} (hab : Commute a b) :
      (a * b)⁻¹ = a⁻¹ * b⁻¹
      source
      theorem AddCommute.neg {G : Type u_1} [SubtractionMonoid G] {a : G} {b : G} (hab : AddCommute a b) :
      -(a + b) = -a + -b
      source
      theorem Commute.inv {G : Type u_1} [DivisionMonoid G] {a : G} {b : G} (hab : Commute a b) :
      (a * b)⁻¹ = a⁻¹ * b⁻¹
      source
      theorem AddCommute.add_neg_cancel {G : Type u_1} [AddGroup G] {a : G} {b : G} (h : AddCommute a b) :
      a + b + -a = b
      source
      theorem Commute.mul_inv_cancel {G : Type u_1} [Group G] {a : G} {b : G} (h : Commute a b) :
      a * b * a⁻¹ = b
      source
      theorem AddCommute.add_neg_cancel_assoc {G : Type u_1} [AddGroup G] {a : G} {b : G} (h : AddCommute a b) :
      a + (b + -a) = b
      source
      theorem Commute.mul_inv_cancel_assoc {G : Type u_1} [Group G] {a : G} {b : G} (h : Commute a b) :
      a * (b * a⁻¹) = b
      source
      theorem succ_nsmul' {M : Type u_2} [AddMonoid M] (a : M) (n : ℕ) :
      (n + 1) • a = n • a + a
      source
      theorem pow_succ' {M : Type u_2} [Monoid M] (a : M) (n : ℕ) :
      a ^ (n + 1) = a ^ n * a
      source
      theorem add_nsmul_sub_zero {M : Type u_2} [AddMonoid M] {n : ℕ} (hn : n ≠ 0) (a : M) :
      a + (n - 1) • a = n • a
      source
      theorem mul_pow_sub_one {M : Type u_2} [Monoid M] {n : ℕ} (hn : n ≠ 0) (a : M) :
      a * a ^ (n - 1) = a ^ n
      source
      theorem nsmul_sub_zero_add {M : Type u_2} [AddMonoid M] {n : ℕ} (hn : n ≠ 0) (a : M) :
      (n - 1) • a + a = n • a
      source
      theorem pow_sub_one_mul {M : Type u_2} [Monoid M] {n : ℕ} (hn : n ≠ 0) (a : M) :
      a ^ (n - 1) * a = a ^ n
      source
      @[simp]
      theorem add_neg_cancel_comm {G : Type u_1} [AddCommGroup G] (a : G) (b : G) :
      a + b + -a = b
      source
      @[simp]
      theorem mul_inv_cancel_comm {G : Type u_1} [CommGroup G] (a : G) (b : G) :
      a * b * a⁻¹ = b
      source
      @[simp]
      theorem add_neg_cancel_comm_assoc {G : Type u_1} [AddCommGroup G] (a : G) (b : G) :
      a + (b + -a) = b
      source
      @[simp]
      theorem mul_inv_cancel_comm_assoc {G : Type u_1} [CommGroup G] (a : G) (b : G) :
      a * (b * a⁻¹) = b