Conjugacy_Action_is_Group_Action_v2

Proved

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

conjugacygroup-actionsgroup-theoryproofwiki

Let $\left({G, \circ}\right)$ be a group whose identity is $e$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Conjugacy_Action_is_Group_Action_v2 {G : Type _} [Group G] (g h k : G) : g * (h * k * h⁻¹) * g⁻¹ = (g * h) * k * (g * h)⁻¹ := by sorry

Source