Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

feat(combinatorics/additive/erdos_ginzburg_ziv): The Erdős–Ginzburg–Ziv theorem #18063

Closed
wants to merge 7 commits into from
Closed

feat(combinatorics/additive/erdos_ginzburg_ziv): The Erdős–Ginzburg–Ziv theorem #18063

wants to merge 7 commits into from

Conversation

YaelDillies
Copy link
Collaborator

@YaelDillies YaelDillies commented Jan 4, 2023 •
edited
Loading

@YaelDillies YaelDillies requested a review from a team as a code owner January 4, 2023 21:57
@YaelDillies YaelDillies added RFC Request for comment t-combinatorics Combinatorics t-number-theory Number theory (also use t-algebra or t-analysis to specialize) labels Jan 4, 2023
@YaelDillies YaelDillies added awaiting-review The author would like community review of the PR blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. and removed RFC Request for comment labels Jan 7, 2023
@YaelDillies @vihdzp
explicit composite case
cd86076 
Co-authored-by: Violeta Hernández <vi.hdz.p@gmail.com>
@kim-em kim-em added the not-too-late This PR was ready at the point mathlib3 was frozen: we will try to merge it and port it to mathlib4 label Jul 16, 2023
@mathlib-dependent-issues-bot mathlib-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Oct 30, 2023
@mathlib-dependent-issues-bot
Copy link
Collaborator

This PR/issue depends on:

@YaelDillies
Copy link
Collaborator Author

Porting this to LeanCamCombi.

@YaelDillies YaelDillies deleted the erdos_ginzburg_ziv branch October 30, 2023 22:53
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@vihdzp vihdzp vihdzp left review comments

Assignees
No one assigned
Labels
awaiting-review The author would like community review of the PR not-too-late This PR was ready at the point mathlib3 was frozen: we will try to merge it and port it to mathlib4 t-combinatorics Combinatorics t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@YaelDillies @mathlib-dependent-issues-bot @vihdzp @kim-em