Commutation_with_Inverse_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 $y$ is invertible. Then $x$ commutes with $y$ $x$ commutes with $y^{-1}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

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

Source