Mathlib.Algebra.GroupWithZero.Commute

Ring.mul_inverse_rev' theorem

{a b : M₀} (h : Commute a b) : inverse (a * b) = inverse b * inverse a

Full source

theorem mul_inverse_rev' {a b : M₀} (h : Commute a b) :
    inverse (a * b) = inverse b * inverse a := by
  by_cases hab : IsUnit (a * b)
  · obtain ⟨⟨a, rfl⟩, b, rfl⟩ := h.isUnit_mul_iff.mp hab
    rw [← Units.val_mul, inverse_unit, inverse_unit, inverse_unit, ← Units.val_mul, mul_inv_rev]
  obtain ha | hb := not_and_or.mp (mt h.isUnit_mul_iff.mpr hab)
  · rw [inverse_non_unit _ hab, inverse_non_unit _ ha, mul_zero]
  · rw [inverse_non_unit _ hab, inverse_non_unit _ hb, zero_mul]

Inverse of Product of Commuting Elements in Monoid with Zero

Informal description

Let $a$ and $b$ be elements of a monoid with zero $M₀$ that commute (i.e., $a * b = b * a$). Then the inverse of their product equals the product of their inverses in reverse order: $\text{inverse}(a * b) = \text{inverse}(b) * \text{inverse}(a)$.

Ring.mul_inverse_rev theorem

{M₀} [CommMonoidWithZero M₀] (a b : M₀) : Ring.inverse (a * b) = inverse b * inverse a

Full source

theorem mul_inverse_rev {M₀} [CommMonoidWithZero M₀] (a b : M₀) :
    Ring.inverse (a * b) = inverse b * inverse a :=
  mul_inverse_rev' (Commute.all _ _)

Inverse of Product in Commutative Monoid with Zero

Informal description

For any elements $a$ and $b$ in a commutative monoid with zero $M₀$, the inverse of their product equals the product of their inverses in reverse order: $\text{inverse}(a \cdot b) = \text{inverse}(b) \cdot \text{inverse}(a)$.

Ring.inverse_pow theorem

(r : M₀) : ∀ n : ℕ, Ring.inverse r ^ n = Ring.inverse (r ^ n)

Full source

lemma inverse_pow (r : M₀) : ∀ n : ℕ, Ring.inverse r ^ n = Ring.inverse (r ^ n)
  | 0 => by rw [pow_zero, pow_zero, Ring.inverse_one]
  | n + 1 => by
    rw [pow_succ', pow_succ, Ring.mul_inverse_rev' ((Commute.refl r).pow_left n),
      Ring.inverse_pow r n]

Power of Inverse Equals Inverse of Power: $(\text{inverse}(r))^n = \text{inverse}(r^n)$

Informal description

For any element $r$ in a monoid with zero $M_0$ and any natural number $n$, the $n$-th power of the inverse of $r$ equals the inverse of the $n$-th power of $r$, i.e., $(\text{inverse}(r))^n = \text{inverse}(r^n)$.

Ring.inverse_pow_mul_eq_iff_eq_mul theorem

{a : M₀} (b c : M₀) (ha : IsUnit a) {k : ℕ} : Ring.inverse a ^ k * b = c ↔ b = a ^ k * c

Full source

lemma inverse_pow_mul_eq_iff_eq_mul {a : M₀} (b c : M₀) (ha : IsUnit a) {k : ℕ} :
    Ring.inverseRing.inverse a ^ k * b = c ↔ b = a ^ k * c := by
  rw [Ring.inverse_pow, Ring.inverse_mul_eq_iff_eq_mul _ _ _ (IsUnit.pow _ ha)]

Equivalence of Inverse Power Multiplication: $(\text{inverse}(a))^k b = c \leftrightarrow b = a^k c$ for a Unit $a$

Informal description

Let $M_0$ be a monoid with zero, and let $a \in M_0$ be a unit. For any elements $b, c \in M_0$ and any natural number $k$, the following equivalence holds: $$(\text{inverse}(a))^k \cdot b = c \quad \text{if and only if} \quad b = a^k \cdot c.$$

Commute.ringInverse_ringInverse theorem

{a b : M₀} (h : Commute a b) : Commute (Ring.inverse a) (Ring.inverse b)

Full source

theorem Commute.ringInverse_ringInverse {a b : M₀} (h : Commute a b) :
    Commute (Ring.inverse a) (Ring.inverse b) :=
  (Ring.mul_inverse_rev' h.symm).symm.trans <| (congr_arg _ h.symm.eq).trans <|
    Ring.mul_inverse_rev' h

Inverses of Commuting Elements Commute

Informal description

For any elements $a$ and $b$ in a monoid with zero $M₀$, if $a$ and $b$ commute (i.e., $a * b = b * a$), then their inverses $\text{inverse}(a)$ and $\text{inverse}(b)$ also commute.

Commute.zero_right theorem

[MulZeroClass G₀] (a : G₀) : Commute a 0

Full source

@[simp]
theorem zero_right [MulZeroClass G₀] (a : G₀) : Commute a 0 :=
  SemiconjBy.zero_right a

Right Commutation with Zero in a MulZeroClass

Informal description

For any element $a$ in a multiplicative structure with zero $G₀$, the element $a$ commutes with zero, i.e., $a \cdot 0 = 0 \cdot a$.

Commute.zero_left theorem

[MulZeroClass G₀] (a : G₀) : Commute 0 a

Full source

@[simp]
theorem zero_left [MulZeroClass G₀] (a : G₀) : Commute 0 a :=
  SemiconjBy.zero_left a a

Zero Commutes with Any Element in a MulZeroClass

Informal description

In a multiplicative structure with zero $G₀$, the zero element $0$ commutes with any element $a \in G₀$, i.e., $0 * a = a * 0$.

Commute.inv_left_iff₀ theorem

: Commute a⁻¹ b ↔ Commute a b

Full source

@[simp]
theorem inv_left_iff₀ : CommuteCommute a⁻¹ b ↔ Commute a b :=
  SemiconjBy.inv_symm_left_iff₀

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

Informal description

For any elements $a$ and $b$ in a group with zero, the inverse $a^{-1}$ 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_left₀ theorem

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

Full source

theorem inv_left₀ (h : Commute a b) : Commute a⁻¹ b :=
  inv_left_iff₀.2 h

Inverse Commutation: $a^{-1} * b = b * a^{-1}$ when $a * b = b * a$

Informal description

For any elements $a$ and $b$ in a group with zero, if $a$ commutes with $b$ (i.e., $a * b = b * a$), then the inverse $a^{-1}$ also commutes with $b$ (i.e., $a^{-1} * b = b * a^{-1}$).

Commute.inv_right_iff₀ theorem

: Commute a b⁻¹ ↔ Commute a b

Full source

@[simp]
theorem inv_right_iff₀ : CommuteCommute a b⁻¹ ↔ Commute a b :=
  SemiconjBy.inv_right_iff₀

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

Informal description

For any elements $a$ and $b$ in a group with zero, the element $a$ commutes with the inverse $b^{-1}$ if and only if $a$ commutes with $b$, i.e., $a * b^{-1} = b^{-1} * a \leftrightarrow a * b = b * a$.

Commute.inv_right₀ theorem

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

Full source

theorem inv_right₀ (h : Commute a b) : Commute a b⁻¹ :=
  inv_right_iff₀.2 h

Commutation with Right Inverse: $a * b = b * a \to a * b^{-1} = b^{-1} * a$

Informal description

For any elements $a$ and $b$ in a group with zero, if $a$ commutes with $b$ (i.e., $a * b = b * a$), then $a$ also commutes with the inverse $b^{-1}$ (i.e., $a * b^{-1} = b^{-1} * a$).

Commute.div_right theorem

(hab : Commute a b) (hac : Commute a c) : Commute a (b / c)

Full source

@[simp]
theorem div_right (hab : Commute a b) (hac : Commute a c) : Commute a (b / c) :=
  SemiconjBy.div_right hab hac

Commutation of an Element with a Quotient of Two Commuting Elements

Informal description

Let $a$, $b$, and $c$ be elements in a group with zero. If $a$ commutes with $b$ (i.e., $a b = b a$) and $a$ commutes with $c$ (i.e., $a c = c a$), then $a$ commutes with $b / c$ (i.e., $a (b / c) = (b / c) a$).

Commute.div_left theorem

(hac : Commute a c) (hbc : Commute b c) : Commute (a / b) c

Full source

@[simp]
theorem div_left (hac : Commute a c) (hbc : Commute b c) : Commute (a / b) c := by
  rw [div_eq_mul_inv]
  exact hac.mul_left hbc.inv_left₀

Commutation of Quotient with Third Element: $(a / b) * c = c * (a / b)$ under Commutativity Conditions

Informal description

Let $a$, $b$, and $c$ be elements in a group with zero. If $a$ commutes with $c$ (i.e., $a * c = c * a$) and $b$ commutes with $c$ (i.e., $b * c = c * b$), then the quotient $a / b$ commutes with $c$ (i.e., $(a / b) * c = c * (a / b)$).

pow_inv_comm₀ theorem

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

Full source

theorem pow_inv_comm₀ (a : G₀) (m n : ℕ) : a⁻¹ ^ m * a ^ n = a ^ n * a⁻¹ ^ m :=
  (Commute.refl a).inv_left₀.pow_pow m n

Commutation of Powers and Inverses: $a^{-m} \cdot a^n = a^n \cdot a^{-m}$

Informal description

For any element $a$ in a group with zero $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$ equals the product of the $n$-th power of $a$ and the $m$-th power of $a^{-1}$, i.e., $a^{-m} \cdot a^n = a^n \cdot a^{-m}$.