Conjugacy_is_Equivalence_Relation

Proved

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

conjugacy-classesequivalence-relationsproofwiki

Conjugacy of group elements is an equivalence relation.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Conjugacy_is_Equivalence_Relation {G : Type _} [Group G] : IsRefl G IsConj ∧ IsSymm G IsConj ∧ IsTrans G IsConj := by sorry

Source