[Merged by Bors] - feat(Combinatorics/SimpleGraph): add definitions and theorems about the coloring of sum graphs by IvanRenison · Pull Request #18677 · leanprover-community/mathlib4

IvanRenison · 2024-11-05T21:46:37Z

github-actions · 2024-11-05T21:47:30Z

messageFile.md

Mathlib/Combinatorics/SimpleGraph/Sum.lean

IvanRenison · 2024-11-14T17:20:01Z

I don't now way the Post PR summary comment is failing

trivial1711

Thanks for the contribution!

Mathlib/Combinatorics/SimpleGraph/Sum.lean

Mathlib/Data/Fin/Basic.lean

Mathlib/Combinatorics/SimpleGraph/Sum.lean

Mathlib/Data/Fin/Basic.lean

github-actions · 2025-01-20T18:54:57Z

messageFile.md

Mathlib/Combinatorics/SimpleGraph/Sum.lean

YaelDillies · 2025-01-20T20:58:34Z

Can you please merge master?

github-actions · 2025-01-24T22:32:34Z

PR summary 65b6264645

Import changes exceeding 2%

%	File
+27.96%	`Mathlib.Combinatorics.SimpleGraph.Sum`

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Combinatorics.SimpleGraph.Sum	515	659	+144 (+27.96%)

Import changes for all files

Files	Import difference
`Mathlib.Combinatorics.SimpleGraph.Sum`	144

Declarations diff

+ Colorable.of_sum_left
+ Colorable.of_sum_right
+ Colorable.sum_max
+ Coloring.sum
+ Coloring.sumEquiv
+ Coloring.sumFin
+ Coloring.sumLeft
+ Coloring.sumLeft_sum
+ Coloring.sumRight
+ Coloring.sumRight_sum
+ Coloring.sum_sumLeft_sumRight
+ chromaticNumber_le_sum_left
+ chromaticNumber_le_sum_right
+ chromaticNumber_sum
+ colorable_sum

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).

kbuzzard · 2025-01-27T14:45:22Z

Thanks!

bors merge

…he coloring of sum graphs (#18677)

mathlib-bors · 2025-01-27T15:35:41Z

Pull request successfully merged into master.

Build succeeded:

* origin/master: (294 commits) feat: equalizers and coequalizers in the category of ind-objects (#21139) doc: turn more links to Stacks into `@[stacks]` tags (#21135) feat(Asymptotics): prove `IsLittleOTVS.add` (#20578) feat(Algebra/Polynomial): `Polynomial.aeval` for product algebras (#21062) chore: import Std in Mathlib.lean (#21126) feat(Data/Matroid/Circuit): fundamental circuits and extensionality (#21145) feat(CategoryTheory/Endofunctor): prove the dual form of Lambek's Lemma on terminal coalgebra (#21140) feat(SetTheory/Game/PGame): rewrite left moves of `-x` as right moves of `x` under binders (#21109) feat(RingTheory/Localization/Pi): localization of a finite direct product is a product of localizations (#19042) doc: fixed notation error in customizing category composition (#21132) feat(Matrix): more lemmas for `PEquiv.toMatrix` (#21143) chore(SupIndep): speedup the `Decidable` instance (#21114) fix(CI): use `Elab.async=false` for late importers workflow (#21147) feat(Topology/Algebra/Indicator): indicator of a clopen is continuous (#20687) feat(Data/Matroid/Rank/Cardinal): Cardinality-valued rank function (#20921) feat(Algebra): `Pi.single_induction` (#21141) chore(BigOperators/Fin): golf a proof (#21131) feat: generalize tangent cone lemmas to TVS (#20859) feat(CategoryTheory): `Comma.snd L R` is final if `R` is final and domains are filtered (#21136) refactor: unapply matrix lemmas (#21091) chore(Algebra/Category): `erw` -> `rw` (#21130) feat(CategoryTheory): filteredness of Comma catgories given finality of one of the functors (#21128) feat(Algebra/Category): `ConcreteCategory` instance for `ModuleCat` (#21125) feat: PSum of finite sorts is finite (#20285) feat: inequality on the integral of a convex function of a RN derivative (#21093) feat: `(v +ᵥ s) -ᵥ (v +ᵥ t) = s -ᵥ t` (#21058) chore: rename the fact that `(∀ a < a₁, a ≤ a₂) ↔ a₁ ≤ a₂` in a dense order (#20317) feat: a `RelHom` preserves directedness (#20080) feat(Combinatorics/SimpleGraph): add definitions and theorems about the coloring of sum graphs (#18677) chore(Data/Matrix/PEquiv): clean up names (#21108) feat(Algebra/Category): `ConcreteCategory` instances for rings (#20815) feat: define Descriptive.Tree (#18763) chore(Data/Complex/Exponential): split trig functions to new file (#21075) feat(Logic/IsEmpty/Relator): empty on sides (#20319) feat(Algebra/Category): `ConcreteCategory` instance for `AlgebraCat` (#21121) feat(NumberTheory/LSeries): results involving partial sums of coefficients (part 1) (#20661) feat(RingTheory/LaurentSeries): add algebraEquiv (#21004) chore(SetTheory/Game/Impartial): golf two proofs (#21074) feat(CategoryTheory/Subpresheaf): preimage/image/range of subpresheaves (#21047) feat(RingTheory/IntegralClosure): `Algebra.IsIntegral` transfers via surjective homomorphisms (#21023) feat(`InformationTheory/Hamming`): Add AddGroup instances (#20994) feat(RingTheory/IntegralClosure): prove `Module.Finite R (adjoin R S)` for finite set `S` of integral elements (#20970) feat(RingTheory/Artinian): `IsUnit a` iff `a ∈ R⁰` for an artinian ring `R` (#21084) feat: separating set in the category of ind-objects (#21082) feat: derivWithin lemmas (#21092) chore(Fintype): golf a proof (#21113) chore: golf using `funext₂` (#21106) chore(Algebra/Group/Submonoid/Operations): move instances to new file (#21067) doc(Algebra/BigOperators/Fin): change 'product' to 'sum' in doc-string of additivised declarations (#21101) doc(ComputeDegree): typos (#21095) ...

* polynomial-sequences: (308 commits) Use the lemma we already added. Minor reordering. This is true even for the trivial ring. Also add the lt versions and the other inj lemma. Also add the basis ne versions. This seems also like it should be simp. Back to sorry free. And the natDegree version. feat: equalizers and coequalizers in the category of ind-objects (#21139) doc: turn more links to Stacks into `@[stacks]` tags (#21135) feat(Asymptotics): prove `IsLittleOTVS.add` (#20578) feat(Algebra/Polynomial): `Polynomial.aeval` for product algebras (#21062) chore: import Std in Mathlib.lean (#21126) feat(Data/Matroid/Circuit): fundamental circuits and extensionality (#21145) feat(CategoryTheory/Endofunctor): prove the dual form of Lambek's Lemma on terminal coalgebra (#21140) feat(SetTheory/Game/PGame): rewrite left moves of `-x` as right moves of `x` under binders (#21109) feat(RingTheory/Localization/Pi): localization of a finite direct product is a product of localizations (#19042) doc: fixed notation error in customizing category composition (#21132) feat(Matrix): more lemmas for `PEquiv.toMatrix` (#21143) chore(SupIndep): speedup the `Decidable` instance (#21114) fix(CI): use `Elab.async=false` for late importers workflow (#21147) feat(Topology/Algebra/Indicator): indicator of a clopen is continuous (#20687) feat(Data/Matroid/Rank/Cardinal): Cardinality-valued rank function (#20921) feat(Algebra): `Pi.single_induction` (#21141) chore(BigOperators/Fin): golf a proof (#21131) feat: generalize tangent cone lemmas to TVS (#20859) feat(CategoryTheory): `Comma.snd L R` is final if `R` is final and domains are filtered (#21136) refactor: unapply matrix lemmas (#21091) chore(Algebra/Category): `erw` -> `rw` (#21130) feat(CategoryTheory): filteredness of Comma catgories given finality of one of the functors (#21128) feat(Algebra/Category): `ConcreteCategory` instance for `ModuleCat` (#21125) feat: PSum of finite sorts is finite (#20285) feat: inequality on the integral of a convex function of a RN derivative (#21093) feat: `(v +ᵥ s) -ᵥ (v +ᵥ t) = s -ᵥ t` (#21058) chore: rename the fact that `(∀ a < a₁, a ≤ a₂) ↔ a₁ ≤ a₂` in a dense order (#20317) feat: a `RelHom` preserves directedness (#20080) feat(Combinatorics/SimpleGraph): add definitions and theorems about the coloring of sum graphs (#18677) chore(Data/Matrix/PEquiv): clean up names (#21108) feat(Algebra/Category): `ConcreteCategory` instances for rings (#20815) feat: define Descriptive.Tree (#18763) chore(Data/Complex/Exponential): split trig functions to new file (#21075) feat(Logic/IsEmpty/Relator): empty on sides (#20319) feat(Algebra/Category): `ConcreteCategory` instance for `AlgebraCat` (#21121) feat(NumberTheory/LSeries): results involving partial sums of coefficients (part 1) (#20661) feat(RingTheory/LaurentSeries): add algebraEquiv (#21004) chore(SetTheory/Game/Impartial): golf two proofs (#21074) feat(CategoryTheory/Subpresheaf): preimage/image/range of subpresheaves (#21047) feat(RingTheory/IntegralClosure): `Algebra.IsIntegral` transfers via surjective homomorphisms (#21023) feat(`InformationTheory/Hamming`): Add AddGroup instances (#20994) feat(RingTheory/IntegralClosure): prove `Module.Finite R (adjoin R S)` for finite set `S` of integral elements (#20970) ...

IvanRenison added 2 commits November 5, 2024 17:22

Add definitions and theorems about the coloring of sum graphs

2ad1c53

Add docstrings and improve proofs

fece94b

github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Nov 5, 2024

Fix typo in docstring of castMax

9b48954

IvanRenison added the t-combinatorics Combinatorics label Nov 5, 2024

urkud reviewed Nov 14, 2024

View reviewed changes

Mathlib/Combinatorics/SimpleGraph/Sum.lean Outdated Show resolved Hide resolved

urkud reviewed Nov 14, 2024

View reviewed changes

Mathlib/Combinatorics/SimpleGraph/Sum.lean Outdated Show resolved Hide resolved

urkud reviewed Nov 14, 2024

View reviewed changes

Mathlib/Combinatorics/SimpleGraph/Sum.lean Outdated Show resolved Hide resolved

urkud reviewed Nov 14, 2024

View reviewed changes

Mathlib/Combinatorics/SimpleGraph/Sum.lean Outdated Show resolved Hide resolved

IvanRenison added 6 commits November 14, 2024 11:51

Merge branch 'master' into IvanRenison/SimpleGraph-sumColoring

2252b9a

Use lowerCamelCase for definitions

5747d40

Re use Coloring.sum for Coloring.sumFin

a1a776f

Colorable.sum_fin → Colorable.sum_max

b064d71

Don't use ChromaticNumber as a namespace

14421d1

Use better names

5ddc634

Add missing @[simp]

578f637

IvanRenison requested a review from urkud November 15, 2024 11:44

Merge branch 'master' into IvanRenison/SimpleGraph-sumColoring

2808b0e

trivial1711 suggested changes Jan 3, 2025

View reviewed changes

trivial1711 added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 3, 2025

IvanRenison added 3 commits January 11, 2025 09:38

Apply names suggestions

a557315

Add suggested theorem and definition

0fe394e

Fix

8377ac8

IvanRenison removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 11, 2025

grunweg changed the title ~~feat(Combinatorics/SimpleGraph): Add definitions and theorems about the coloring of sum graphs~~ feat(Combinatorics/SimpleGraph): add definitions and theorems about the coloring of sum graphs Jan 20, 2025

kbuzzard reviewed Jan 20, 2025

View reviewed changes

kbuzzard added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 20, 2025

grunweg reviewed Jan 20, 2025

View reviewed changes

Mathlib/Combinatorics/SimpleGraph/Sum.lean Outdated Show resolved Hide resolved

YaelDillies reviewed Jan 20, 2025

View reviewed changes

Mathlib/Combinatorics/SimpleGraph/Sum.lean Outdated Show resolved Hide resolved

Apply suggestions

4b87039

IvanRenison removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 20, 2025

YaelDillies reviewed Jan 20, 2025

View reviewed changes

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 20, 2025

Apply suggestions

1e23bb9

YaelDillies reviewed Jan 20, 2025

View reviewed changes

IvanRenison added 2 commits January 24, 2025 19:29

Apply suggestions

f49bf1d

Merge branch 'master' into IvanRenison/SimpleGraph-sumColoring

65b6264

IvanRenison removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 24, 2025

ghost added the ready-to-merge This PR has been sent to bors. label Jan 27, 2025

mathlib-bors bot pushed a commit that referenced this pull request Jan 27, 2025

feat(Combinatorics/SimpleGraph): add definitions and theorems about t…

da67df3

…he coloring of sum graphs (#18677)

mathlib-bors bot changed the title ~~feat(Combinatorics/SimpleGraph): add definitions and theorems about the coloring of sum graphs~~ [Merged by Bors] - feat(Combinatorics/SimpleGraph): add definitions and theorems about the coloring of sum graphs Jan 27, 2025

mathlib-bors bot closed this Jan 27, 2025

mathlib-bors bot deleted the IvanRenison/SimpleGraph-sumColoring branch January 27, 2025 15:35

Conversation

IvanRenison commented Nov 5, 2024

Uh oh!

github-actions bot commented Nov 5, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

IvanRenison commented Nov 14, 2024

Uh oh!

trivial1711 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!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

github-actions bot commented Jan 20, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

YaelDillies commented Jan 20, 2025

Uh oh!

github-actions bot commented Jan 24, 2025

PR summary 65b6264645

Import changes for modified files

Declarations diff

Uh oh!

kbuzzard commented Jan 27, 2025

Uh oh!

mathlib-bors bot commented Jan 27, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

github-actions bot commented Nov 5, 2024 •

edited

Loading