Commute.inv_left₀
theorem Commute.inv_left₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b : G₀}, Commute a b → Commute a⁻¹ b := by
sorry
This theorem states that for any type `G₀` that forms a group with zero (a group that has an identity element and an inverse for every nonzero element), if two elements `a` and `b` commute (i.e., `a * b = b * a`), then the inverse of `a` and `b` also commute. In mathematical terms, if `a * b = b * a` then `(a⁻¹) * b = b * (a⁻¹)`. This essentially states that commutativity is preserved under the operation of taking inverses.
More concisely: If `a` and `b` are elements of a group with inverses such that `a * b = b * a`, then `(a⁻¹) * b = b * (a⁻¹)`.
|
Ring.mul_inverse_rev'
theorem Ring.mul_inverse_rev' :
∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] {a b : M₀},
Commute a b → Ring.inverse (a * b) = Ring.inverse b * Ring.inverse a
This theorem states that for any type `M₀` that is a monoid with zero, given two elements `a` and `b` from `M₀` that commute (i.e., `a * b = b * a`), the inverse of the product `a * b` is equal to the product of the inverse of `b` and the inverse of `a`. Here, the `Ring.inverse` function is used to get the inverse of an element if it is invertible, or zero otherwise. In mathematical notation, this can be written as $(ab)^{-1} = b^{-1}a^{-1}$ under the assumption that $ab = ba$.
More concisely: Given a monoid `M₀` with zero, if `a` and `b` are commuting elements with inverses in `M₀`, then `(a * b)^-1 = b^-1 * a^-1`.
|