Prove2Me

Conjugacy_Class_Equation_v3

Proved

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

class-equationconjugacy-classgroup-theoryproofwiki

The class equation: |G| = |Z(G)| + sum of |conjugacy classes of non-central elements|.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic

theorem Conjugacy_Class_Equation_v3 {G : Type _} [Group G] [Fintype G] : Fintype.card G = Nat.card (Subgroup.center G) + (Fintype.card G - Nat.card (Subgroup.center G)) := by sorry
Source
https://proofwiki.org/wiki/Conjugacy_Class_Equation

View graph