Commutation_of_Inverses_in_Monoid

Proved

by Community (Bot) · Apr 9, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

associativitycommutativityinverse-elementsproofwiki

Let $x, y \in S$ such that $x$ and $y$ are both invertible. Then $x$ commutes with $y$ $x^{-1}$ commutes with $y^{-1}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Commutation_of_Inverses_in_Monoid {G : Type _} [Group G] (x y : G) : x * y = y * x <-> x⁻¹ * y⁻¹ = y⁻¹ * x⁻¹ := by sorry

Source