Polya_counting

[515801431]

This PR introduces basic definitions and results about colorings under permutation group actions.
A coloring is defined as a function X → Y, and the permutation group Equiv.Perm X acts on colorings by precomposition:

(g • c) x = c (g⁻¹ • x)

This formalizes the natural action of relabeling the elements of X.

Main definitions

MulAction (Equiv.Perm X) (X → Y):
The action of the permutation group on colorings via precomposition.

coloringEquiv (c₁ c₂ : X → Y) : Prop:
Two colorings are equivalent if they lie in the same orbit under this action, i.e.
∃ f : Equiv.Perm X, f • c₁ = c₂.

Main results

smul_eq_iff_mem_stabilizer:
Characterizes when two group actions on the same coloring are equal, showing that
g • c = f • c ↔ f⁻¹ * g ∈ stabilizer c.

coloringEquiv_equivalence:
Proves that coloringEquiv defines an equivalence relation on X → Y.

orbit_size_eq_index:
Reformulates the orbit–stabilizer theorem in the context of colorings:

|orbit c| = |Perm X| / |stabilizer c|

Motivation

These results provide foundational infrastructure for studying Burnside’s lemma and Pólya’s enumeration theorem in Mathlib, where the enumeration of distinct colorings up to symmetry plays a central role.

[github-actions]

PR summary c48ea032ed

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Combinatorics.Enumerative.Polya (new file)	732

---

Declarations diff

+ coloringEquiv
+ coloringEquiv_equivalence
+ instance : MulAction (Equiv.Perm X) (X → Y)
+ orbit_size_eq_index
+ smul_eq_iff_mem_stabilizer

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[IvanRenison]

Hi, I see you are making very similar changes in this pull request and in #30527, you should only keep one of them, and close the other one