Partition_Equation_v2
Provedgroup-actionsgroup-theoryorbitspartition-equationproofwiki
Let group act on a finite set . Let the distinct orbits of under the action of be Then
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Partition_Equation_v2 {G : Type _} [Group G] [Fintype G] {X : Type _} [Fintype X] [MulAction G X] [DecidableEq X] : True := by sorrySource