Mathlib.Algebra.Group.Commute.Basic

SemiconjBy.function_semiconj_mul_left theorem

(h : SemiconjBy a b c) : Semiconj (a * ·) (b * ·) (c * ·)

Full source

@[to_additive]
lemma SemiconjBy.function_semiconj_mul_left (h : SemiconjBy a b c) :
    Semiconj (a * ·) (b * ·) (c * ·) := fun j ↦ by simp only [← mul_assoc, h.eq]

Semiconjugacy of Left Multiplication Functions under Semiconjugate Elements

Informal description

Given elements $a, b, c$ in a monoid such that $a$ semiconjugates $b$ and $c$ (i.e., $ab = bc$), the left multiplication functions $(a \cdot)$, $(b \cdot)$, and $(c \cdot)$ satisfy the semiconjugacy relation: $(a \cdot) \circ (b \cdot) = (c \cdot) \circ (a \cdot)$.

Commute.function_commute_mul_left theorem

(h : Commute a b) : Function.Commute (a * ·) (b * ·)

Full source

@[to_additive]
lemma Commute.function_commute_mul_left (h : Commute a b) : Function.Commute (a * ·) (b * ·) :=
  SemiconjBy.function_semiconj_mul_left h

Commutation of Left Multiplication Functions for Commuting Elements

Informal description

If two elements $a$ and $b$ in a monoid commute (i.e., $ab = ba$), then their corresponding left multiplication functions $(a \cdot)$ and $(b \cdot)$ also commute, meaning $(a \cdot) \circ (b \cdot) = (b \cdot) \circ (a \cdot)$.

SemiconjBy.function_semiconj_mul_right_swap theorem

(h : SemiconjBy a b c) : Function.Semiconj (· * a) (· * c) (· * b)

Full source

@[to_additive]
lemma SemiconjBy.function_semiconj_mul_right_swap (h : SemiconjBy a b c) :
    Function.Semiconj (· * a) (· * c) (· * b) := fun j ↦ by simp only [mul_assoc, ← h.eq]

Semiconjugation of Right Multiplication Functions under Semiconjugate Elements

Informal description

Given elements $a, b, c$ in a monoid such that $a$ semiconjugates $b$ and $c$ (i.e., $a * b = c * a$), the right multiplication function $x \mapsto x * a$ semiconjugates the right multiplication functions $x \mapsto x * c$ and $x \mapsto x * b$. In other words, for all $x$ in the monoid, $(x * c) * a = (x * a) * b$.

Commute.function_commute_mul_right theorem

(h : Commute a b) : Function.Commute (· * a) (· * b)

Full source

@[to_additive]
lemma Commute.function_commute_mul_right (h : Commute a b) : Function.Commute (· * a) (· * b) :=
  SemiconjBy.function_semiconj_mul_right_swap h

Commutation of Right Multiplication Functions for Commuting Elements

Informal description

If two elements $a$ and $b$ in a monoid commute (i.e., $ab = ba$), then their corresponding right multiplication functions $( \cdot \, a)$ and $( \cdot \, b)$ also commute, meaning $( \cdot \, a) \circ ( \cdot \, b) = ( \cdot \, b) \circ ( \cdot \, a)$.

Commute.inv_inv theorem

: Commute a b → Commute a⁻¹ b⁻¹

Full source

@[to_additive]
protected theorem inv_inv : Commute a b → Commute a⁻¹ b⁻¹ :=
  SemiconjBy.inv_inv_symm

Commutation of Inverses in a Division Monoid

Informal description

If two elements $a$ and $b$ in a division monoid commute (i.e., $ab = ba$), then their inverses $a^{-1}$ and $b^{-1}$ also commute (i.e., $a^{-1}b^{-1} = b^{-1}a^{-1}$).

Commute.inv_inv_iff theorem

: Commute a⁻¹ b⁻¹ ↔ Commute a b

Full source

@[to_additive (attr := simp)]
theorem inv_inv_iff : CommuteCommute a⁻¹ b⁻¹ ↔ Commute a b :=
  SemiconjBy.inv_inv_symm_iff

Inverse Commutation Equivalence: $a^{-1}b^{-1} = b^{-1}a^{-1} \leftrightarrow ab = ba$

Informal description

For any two elements $a$ and $b$ in a division monoid, the inverses $a^{-1}$ and $b^{-1}$ commute if and only if $a$ and $b$ commute, i.e., $a^{-1}b^{-1} = b^{-1}a^{-1} \leftrightarrow ab = ba$.

Commute.div_mul_div_comm theorem

(hbd : Commute b d) (hbc : Commute b⁻¹ c) : a / b * (c / d) = a * c / (b * d)

Full source

@[to_additive]
protected theorem div_mul_div_comm (hbd : Commute b d) (hbc : Commute b⁻¹ c) :
    a / b * (c / d) = a * c / (b * d) := by
  simp_rw [div_eq_mul_inv, mul_inv_rev, hbd.inv_inv.symm.eq, hbc.mul_mul_mul_comm]

Division-Multiplication Commutation Identity: $\frac{a}{b} \cdot \frac{c}{d} = \frac{a \cdot c}{b \cdot d}$ under Commutation Conditions

Informal description

Let $a, b, c, d$ be elements of a division monoid such that $b$ commutes with $d$ (i.e., $bd = db$) and $b^{-1}$ commutes with $c$ (i.e., $b^{-1}c = cb^{-1}$). Then the following equality holds: \[ \frac{a}{b} \cdot \frac{c}{d} = \frac{a \cdot c}{b \cdot d} \]

Commute.mul_div_mul_comm theorem

(hcd : Commute c d) (hbc : Commute b c⁻¹) : a * b / (c * d) = a / c * (b / d)

Full source

@[to_additive]
protected theorem mul_div_mul_comm (hcd : Commute c d) (hbc : Commute b c⁻¹) :
    a * b / (c * d) = a / c * (b / d) :=
  (hcd.div_mul_div_comm hbc.symm).symm

Multiplication-Division Commutation Identity: $\frac{ab}{cd} = \frac{a}{c} \cdot \frac{b}{d}$ under Commutation Conditions

Informal description

Let $a, b, c, d$ be elements of a division monoid such that $c$ commutes with $d$ (i.e., $cd = dc$) and $b$ commutes with $c^{-1}$ (i.e., $bc^{-1} = c^{-1}b$). Then the following equality holds: \[ \frac{a \cdot b}{c \cdot d} = \frac{a}{c} \cdot \frac{b}{d} \]

Commute.div_div_div_comm theorem

(hbc : Commute b c) (hbd : Commute b⁻¹ d) (hcd : Commute c⁻¹ d) : a / b / (c / d) = a / c / (b / d)

Full source

@[to_additive]
protected theorem div_div_div_comm (hbc : Commute b c) (hbd : Commute b⁻¹ d) (hcd : Commute c⁻¹ d) :
    a / b / (c / d) = a / c / (b / d) := by
  simp_rw [div_eq_mul_inv, mul_inv_rev, inv_inv, hbd.symm.eq, hcd.symm.eq,
    hbc.inv_inv.mul_mul_mul_comm]

Division Chain Commutation Identity: $\frac{a/b}{c/d} = \frac{a/c}{b/d}$ under Commutation Conditions

Informal description

Let $a, b, c, d$ be elements of a division monoid such that: 1. $b$ commutes with $c$ (i.e., $bc = cb$), 2. $b^{-1}$ commutes with $d$ (i.e., $b^{-1}d = db^{-1}$), 3. $c^{-1}$ commutes with $d$ (i.e., $c^{-1}d = dc^{-1}$). Then the following equality holds: \[ \frac{a/b}{c/d} = \frac{a/c}{b/d} \]

Commute.inv_left_iff theorem

: Commute a⁻¹ b ↔ Commute a b

Full source

@[to_additive (attr := simp)]
lemma inv_left_iff : CommuteCommute a⁻¹ b ↔ Commute a b := SemiconjBy.inv_symm_left_iff

Inverse Commutation Criterion: $a^{-1}b = b a^{-1} \leftrightarrow a b = b a$

Informal description

For elements $a$ and $b$ in a division monoid, the inverse of $a$ commutes with $b$ if and only if $a$ commutes with $b$, i.e., $a^{-1}b = b a^{-1} \leftrightarrow a b = b a$.

Commute.inv_right_iff theorem

: Commute a b⁻¹ ↔ Commute a b

Full source

@[to_additive (attr := simp)]
lemma inv_right_iff : CommuteCommute a b⁻¹ ↔ Commute a b := SemiconjBy.inv_right_iff

Commutation with Inverse: $a \cdot b^{-1} = b^{-1} \cdot a \leftrightarrow a \cdot b = b \cdot a$

Informal description

For elements $a$ and $b$ in a division monoid, $a$ commutes with $b^{-1}$ if and only if $a$ commutes with $b$. In other words, $a \cdot b^{-1} = b^{-1} \cdot a$ holds precisely when $a \cdot b = b \cdot a$.

Commute.inv_mul_cancel theorem

(h : Commute a b) : a⁻¹ * b * a = b

Full source

@[to_additive]
protected lemma inv_mul_cancel (h : Commute a b) : a⁻¹ * b * a = b := by
  rw [h.inv_left.eq, inv_mul_cancel_right]

Conjugation by Inverse of Commuting Element: $a^{-1} b a = b$ when $a$ and $b$ commute

Informal description

For any two commuting elements $a$ and $b$ in a division monoid, the operation $a^{-1} b a$ simplifies to $b$.

Commute.inv_mul_cancel_assoc theorem

(h : Commute a b) : a⁻¹ * (b * a) = b

Full source

@[to_additive]
lemma inv_mul_cancel_assoc (h : Commute a b) : a⁻¹ * (b * a) = b := by
  rw [← mul_assoc, h.inv_mul_cancel]

Associative Conjugation by Inverse of Commuting Element: $a^{-1} (b a) = b$ when $a$ and $b$ commute

Informal description

For any two commuting elements $a$ and $b$ in a division monoid, the operation $a^{-1} \cdot (b \cdot a)$ simplifies to $b$.

Commute.conj_iff theorem

(h : G) : Commute (h * a * h⁻¹) (h * b * h⁻¹) ↔ Commute a b

Full source

@[to_additive (attr := simp)]
protected theorem conj_iff (h : G) : CommuteCommute (h * a * h⁻¹) (h * b * h⁻¹) ↔ Commute a b :=
  SemiconjBy.conj_iff

Conjugation Preserves Commutation: $h a h^{-1}$ and $h b h^{-1}$ Commute iff $a$ and $b$ Commute

Informal description

For any element $h$ in a group $G$, the conjugate elements $h a h^{-1}$ and $h b h^{-1}$ commute if and only if the original elements $a$ and $b$ commute. In other words, $h a h^{-1} \cdot h b h^{-1} = h b h^{-1} \cdot h a h^{-1}$ if and only if $a b = b a$.

Commute.conj theorem

(comm : Commute a b) (h : G) : Commute (h * a * h⁻¹) (h * b * h⁻¹)

Full source

@[to_additive]
protected theorem conj (comm : Commute a b) (h : G) : Commute (h * a * h⁻¹) (h * b * h⁻¹) :=
  (Commute.conj_iff h).mpr comm

Conjugation Preserves Commutation of Elements

Informal description

For any two elements $a$ and $b$ in a group $G$ that commute (i.e., $ab = ba$), and for any element $h \in G$, the conjugate elements $h a h^{-1}$ and $h b h^{-1}$ also commute. That is, $(h a h^{-1})(h b h^{-1}) = (h b h^{-1})(h a h^{-1})$.

Commute.zpow_right theorem

(h : Commute a b) (m : ℤ) : Commute a (b ^ m)

Full source

@[to_additive (attr := simp)]
lemma zpow_right (h : Commute a b) (m : ℤ) : Commute a (b ^ m) := SemiconjBy.zpow_right h m

Commutation with Integer Powers: $a$ Commutes with $b^m$

Informal description

For any two elements $a$ and $b$ in a group $G$ that commute (i.e., $ab = ba$), and for any integer $m$, the element $a$ commutes with the $m$-th power of $b$, i.e., $a(b^m) = (b^m)a$.

Commute.zpow_left theorem

(h : Commute a b) (m : ℤ) : Commute (a ^ m) b

Full source

@[to_additive (attr := simp)]
lemma zpow_left (h : Commute a b) (m : ℤ) : Commute (a ^ m) b := (h.symm.zpow_right m).symm

Commutation with Integer Powers: $a^m$ Commutes with $b$

Informal description

For any two elements $a$ and $b$ in a group $G$ that commute (i.e., $ab = ba$), and for any integer $m$, the $m$-th power of $a$ commutes with $b$, i.e., $(a^m)b = b(a^m)$.

Commute.zpow_zpow theorem

(h : Commute a b) (m n : ℤ) : Commute (a ^ m) (b ^ n)

Full source

@[to_additive] lemma zpow_zpow (h : Commute a b) (m n : ℤ) : Commute (a ^ m) (b ^ n) :=
  (h.zpow_left m).zpow_right n

Commutation of Integer Powers: $(a^m)(b^n) = (b^n)(a^m)$

Informal description

For any two elements $a$ and $b$ in a group $G$ that commute (i.e., $ab = ba$), and for any integers $m$ and $n$, the $m$-th power of $a$ commutes with the $n$-th power of $b$, i.e., $(a^m)(b^n) = (b^n)(a^m)$.

Commute.self_zpow theorem

: Commute a (a ^ n)

Full source

@[to_additive] lemma self_zpow : Commute a (a ^ n) := (Commute.refl a).zpow_right n

Self-Commutation with Integer Powers: $a$ Commutes with $a^n$

Informal description

For any element $a$ in a group $G$ and any integer $n$, the element $a$ commutes with its own $n$-th power, i.e., $a(a^n) = (a^n)a$.

Commute.zpow_self theorem

: Commute (a ^ n) a

Full source

@[to_additive] lemma zpow_self : Commute (a ^ n) a := (Commute.refl a).zpow_left n

Commutation of Integer Power with Element: $(a^n)a = a(a^n)$

Informal description

For any element $a$ in a group $G$ and any integer $n$, the $n$-th power of $a$ commutes with $a$ itself, i.e., $(a^n)a = a(a^n)$.

Commute.zpow_zpow_self theorem

: Commute (a ^ m) (a ^ n)

Full source

@[to_additive] lemma zpow_zpow_self : Commute (a ^ m) (a ^ n) := (Commute.refl a).zpow_zpow m n

Commutation of Integer Powers of the Same Element: $(a^m)(a^n) = (a^n)(a^m)$

Informal description

For any element $a$ in a group $G$ and any integers $m$ and $n$, the $m$-th power of $a$ commutes with the $n$-th power of $a$, i.e., $(a^m)(a^n) = (a^n)(a^m)$.

pow_inv_comm theorem

(a : G) (m n : ℕ) : a⁻¹ ^ m * a ^ n = a ^ n * a⁻¹ ^ m

Full source

@[to_additive] lemma pow_inv_comm (a : G) (m n : ℕ) : a⁻¹ ^ m * a ^ n = a ^ n * a⁻¹ ^ m :=
  (Commute.refl a).inv_left.pow_pow _ _

Commutation of Powers of Inverse and Element: $(a^{-1})^m \cdot a^n = a^n \cdot (a^{-1})^m$

Informal description

For any element $a$ in a group $G$ and any natural numbers $m$ and $n$, the product of the $m$-th power of $a^{-1}$ and the $n$-th power of $a$ is equal to the product of the $n$-th power of $a$ and the $m$-th power of $a^{-1}$. That is, $(a^{-1})^m \cdot a^n = a^n \cdot (a^{-1})^m$.