Inverse_of_Commuting_Pair

Proved

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

commutativitygroup-theoryinverse-of-commuting-pairmonoidsproofwiki

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

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

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

Source