feat(GroupTheory): summation over a conjugacy class by Yu-Misaka · Pull Request #41326 · leanprover-community/mathlib4

Yu-Misaka · 2026-07-03T14:01:17Z

This PR proves ConjClasses.sum_carrier_mul_left: Summing f (g * h) over h in the conjugacy class of g equals summing f (h * g).

This result can potentially help prove, for example, ∑ h ∈ (ConjClasses.mk g).carrier, ρ h is intertwining in the settings of representation theory.

github-actions · 2026-07-03T14:02:35Z

PR summary 83865bda6f

Import changes exceeding 2%

%	File
+4.43%	`Mathlib.Algebra.Group.Conj`

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Group.Conj	361	377	+16 (+4.43%)

Import changes for all files

Files	Import difference
`Mathlib.Algebra.Group.Conj` `Mathlib.Algebra.GroupWithZero.Conj`	16

Declarations diff (regex)

+ invOn_conj
+ isConj_inv_mul_mul_left
+ isConj_inv_mul_mul_right
+ isConj_mul_mul_inv_left
+ isConj_mul_mul_inv_right
+ mapsTo_conj
+ mk_conj
+ mk_conj_assoc
+ mk_inv_conj
+ mk_inv_conj_assoc
+ prod_carrier_conj
+ prod_carrier_mul_left

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 83865bd).

+24 new declarations
−0 removed declarations

+AddConjClasses.mapsTo_addConj
+AddConjClasses.mk_addConj
+AddConjClasses.mk_addConj_assoc
+AddConjClasses.mk_neg_addConj
+AddConjClasses.mk_neg_addConj_assoc
+AddConjClasses.negOn_addConj
+ConjClasses.invOn_conj
+ConjClasses.mapsTo_conj
+ConjClasses.mk_conj
+ConjClasses.mk_conj_assoc
+ConjClasses.mk_inv_conj
+ConjClasses.mk_inv_conj_assoc
+ConjClasses.prod_carrier_conj
+ConjClasses.prod_carrier_mul_left
+ConjClasses.sum_carrier_conj
+ConjClasses.sum_carrier_mul_left
+isAddConj_add_add_neg_left
+isAddConj_add_add_neg_right
+isAddConj_neg_add_add_left
+isAddConj_neg_add_add_right
+isConj_inv_mul_mul_left
+isConj_inv_mul_mul_right
+isConj_mul_mul_inv_left
+isConj_mul_mul_inv_right

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 83865bda6f
Reference commit bfefa91d21

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/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).

Co-authored-by: Weiyi Wang <wwylele@gmail.com>

wwylele

Otherwise looks good to me

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Yu-Misaka · 2026-07-17T04:42:07Z

+  simp [mk_eq_mk_iff_isConj]
+
+@[to_additive]
+theorem mapsTo_conj {α : Type*} [Group α] (k : α) (c : ConjClasses α) :


Should I inline this lemma? (I am referring to mapsTo_conj)

It's much easier for me to answer if you make a multiline comment including the statement!

I would say you should replace the InjOn and BijOn lemmas by a single InvOn one

Ah, sure I'll do multiline next time. And thanks for your advice, implemented!

(I kept the MapsTo lemma though, as it is needed in Finset.prod_nbij and can't be derived from InvOn)

I kept the MapsTo lemma though, as it is needed in Finset.prod_nbij and can't be derived from InvOn

This seems bad. Mathematically it should, right? Can you complain on Zulip that the definition of InvOn is wrong?

lol, sure! (Zulip link: #mathlib4 > Should Set.InvOn imply Set.MapsTo?)

For now, can you strengthen this to BijOn?

No problem ;)

(I'm a bit busy this week, will get back to you as soon as possible)

YaelDillies · 2026-07-17T08:27:05Z

Don't forget to resolve the comments that you have satisfactorily addressed!

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

YaelDillies · 2026-07-21T12:34:38Z

+lemma mk_conj {α : Type*} [Group α] (m x : α) :
+    ConjClasses.mk (m * x * m⁻¹) = ConjClasses.mk x := by


Can you use the same naming convention here and below? You can prime the reassociated lemmas to disambiguate

init

1de92bd

github-actions Bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Jul 3, 2026

github-actions Bot added the t-group-theory Group theory label Jul 3, 2026

wwylele reviewed Jul 3, 2026

View reviewed changes

Comment thread Mathlib/Algebra/Group/Conj.lean Outdated

Comment thread Mathlib/GroupTheory/ClassEquation.lean Outdated

Yu-Misaka and others added 2 commits July 3, 2026 23:01

Update Mathlib/Algebra/Group/Conj.lean

26c73d4

Co-authored-by: Weiyi Wang <wwylele@gmail.com>

Finset.prod & to_additive

ba384bc

wwylele reviewed Jul 3, 2026

View reviewed changes

Comment thread Mathlib/Algebra/Group/Conj.lean Outdated

Comment thread Mathlib/GroupTheory/ClassEquation.lean Outdated

Yu-Misaka added 2 commits July 4, 2026 11:57

address suggestions

61daf68

Merge branch 'master' into conjClass_sum

02db752

wwylele reviewed Jul 4, 2026

View reviewed changes

Comment thread Mathlib/Algebra/Group/ConjFinite.lean Outdated

to_additive on H

4cd0d96

tb65536 reviewed Jul 4, 2026

View reviewed changes

Comment thread Mathlib/Algebra/Group/ConjFinite.lean Outdated

tb65536 reviewed Jul 4, 2026

View reviewed changes

Comment thread Mathlib/Algebra/Group/Conj.lean Outdated

Yu-Misaka added 7 commits July 4, 2026 21:38

avoid change, rename to mk_conj

389298a

allow any conjugacy classes

794977c

nameing

fb18afa

style

ac86d63

style

91c81ba

Merge branch 'master' into conjClass_sum

b96b40a

Merge branch 'master' into conjClass_sum

59b2461

Yu-Misaka mentioned this pull request Jul 8, 2026

feat(RepresentationTheory/Character): add integral result for character and conjugacy classes #41489

Draft

2 tasks

Yu-Misaka requested review from YaelDillies and tb65536 and removed request for tb65536 July 9, 2026 11:09

YaelDillies reviewed Jul 15, 2026

View reviewed changes

Comment thread Mathlib/Algebra/Group/Conj.lean Outdated

Comment thread Mathlib/Algebra/Group/Conj.lean Outdated

Comment thread Mathlib/Algebra/Group/ConjFinite.lean Outdated

Comment thread Mathlib/Algebra/Group/ConjFinite.lean Outdated

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 15, 2026

YaelDillies self-assigned this Jul 15, 2026

Yu-Misaka and others added 2 commits July 16, 2026 13:36

Update Mathlib/Algebra/Group/ConjFinite.lean

6eaa59a

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

implement suggestions

b41a188

one liner

8aebd44

Yu-Misaka removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 17, 2026

Merge branch 'master' into conjClass_sum

8f94148

Yu-Misaka commented Jul 17, 2026

View reviewed changes

del mk_conj

68a07b2

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 17, 2026

replace BijOn with InvOn

72406b9

Yu-Misaka removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 19, 2026

YaelDillies reviewed Jul 19, 2026

View reviewed changes

Comment thread Mathlib/Algebra/Group/Conj.lean Outdated

YaelDillies reviewed Jul 19, 2026

View reviewed changes

Comment thread Mathlib/Algebra/Group/ConjFinite.lean

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 19, 2026

Yu-Misaka and others added 2 commits July 19, 2026 14:17

Update Mathlib/Algebra/Group/Conj.lean

baf5cee

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

name

83865bd

YaelDillies reviewed Jul 21, 2026

View reviewed changes

		lemma mk_conj {α : Type*} [Group α] (m x : α) :
		ConjClasses.mk (m * x * m⁻¹) = ConjClasses.mk x := by

Uh oh!

Conversation

Yu-Misaka commented Jul 3, 2026 • edited by YaelDillies Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Jul 3, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 83865bda6f

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean)

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

wwylele left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Yu-Misaka Jul 17, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

YaelDillies Jul 17, 2026

Choose a reason for hiding this comment

Uh oh!

YaelDillies Jul 17, 2026

Choose a reason for hiding this comment

Uh oh!

Yu-Misaka Jul 19, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

YaelDillies Jul 19, 2026

Choose a reason for hiding this comment

Uh oh!

Yu-Misaka Jul 19, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

YaelDillies Jul 21, 2026

Choose a reason for hiding this comment

Uh oh!

Yu-Misaka Jul 23, 2026

Choose a reason for hiding this comment

Uh oh!

YaelDillies commented Jul 17, 2026

Uh oh!

Uh oh!

Uh oh!

YaelDillies Jul 21, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Yu-Misaka commented Jul 3, 2026 •

edited by YaelDillies

Loading

github-actions Bot commented Jul 3, 2026 •

edited

Loading

Yu-Misaka Jul 17, 2026 •

edited

Loading

Yu-Misaka Jul 19, 2026 •

edited

Loading

Yu-Misaka Jul 19, 2026 •

edited

Loading