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

feat(combinatorics/simple_graph): Triangle counting #19206

Closed
wants to merge 4 commits into from

Conversation

YaelDillies
Copy link
Collaborator

@YaelDillies YaelDillies commented Jun 19, 2023

Prove the triangle counting lemma. Definitions that are internal to the proof are made private.


I would like ideas on the lemma names

Open in Gitpod

Prove the triangle counting lemma. Definitions that are internal to the proof are made private.
@YaelDillies YaelDillies requested a review from a team as a code owner June 19, 2023 21:29
@YaelDillies YaelDillies added RFC Request for comment awaiting-review The author would like community review of the PR t-combinatorics Combinatorics labels Jun 19, 2023
@github-actions github-actions bot added the modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. label Jun 19, 2023
@eric-wieser eric-wieser 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 15, 2023
@YaelDillies
Copy link
Collaborator Author

Ported as leanprover-community/mathlib4#8896.

@YaelDillies YaelDillies closed this Dec 8, 2023
@YaelDillies YaelDillies deleted the triangle_counting branch December 8, 2023 11:19
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
awaiting-review The author would like community review of the PR modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization 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 RFC Request for comment t-combinatorics Combinatorics
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants