Conjugacy_Action_on_Identity

Proved

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

conjugacygroup-actionsgroup-theoryidentityproofwiki

Let $G$ be a group whose identity is $e$ . For the conjugacy action $\order {\Orb e} = 1$ and thus $\Stab e = G$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Conjugacy_Action_on_Identity {G : Type _} [Group G] (g : G) : g * 1 * g⁻¹ = 1 := by sorry

Source