Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat(combinatorics/simple_graph/adj_matrix): more lemmas #9021

Closed
wants to merge 25 commits into from
Closed

[Merged by Bors] - feat(combinatorics/simple_graph/adj_matrix): more lemmas #9021

wants to merge 25 commits into from

Conversation

l534zhan
Copy link
Collaborator

@l534zhan l534zhan commented Sep 6, 2021

Open in Gitpod

@l534zhan
Copy link
Collaborator Author

l534zhan commented Sep 6, 2021 •
edited
Loading

This PR is a part of my project. See https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Contribute.20a.20project.20on.20Hadamard.20matrices.

This PR weakens the conditions for adjacency matrices and adds more lemmas, as discussed in https://leanprover.zulipchat.com/#narrow/stream/252551-graph-theory/topic/adj_matrix.

Some variable names used in the original file can be confusing and are inconsistent with other parts of mathlib. I changed such names.

@l534zhan l534zhan requested a review from kmill September 6, 2021 00:12
kmill
kmill reviewed Sep 6, 2021
View reviewed changes
Copy link
Collaborator

@kmill kmill left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Some comments so far

src/combinatorics/simple_graph/adj_matrix.lean Outdated Show resolved Hide resolved
src/combinatorics/simple_graph/adj_matrix.lean Outdated Show resolved Hide resolved
src/combinatorics/simple_graph/adj_matrix.lean Outdated Show resolved Hide resolved
src/combinatorics/simple_graph/adj_matrix.lean Outdated Show resolved Hide resolved
src/combinatorics/simple_graph/adj_matrix.lean Outdated Show resolved Hide resolved
src/combinatorics/simple_graph/adj_matrix.lean Outdated Show resolved Hide resolved
src/combinatorics/simple_graph/adj_matrix.lean Show resolved Hide resolved
src/combinatorics/simple_graph/adj_matrix.lean Show resolved Hide resolved
src/combinatorics/simple_graph/adj_matrix.lean Outdated Show resolved Hide resolved
l534zhan and others added 5 commits September 6, 2021 16:03
@l534zhan @kmill
Update src/combinatorics/simple_graph/adj_matrix.lean
08052e3 
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
@l534zhan @kmill
Update src/combinatorics/simple_graph/adj_matrix.lean
43e9e11 
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
@l534zhan @kmill
Update src/combinatorics/simple_graph/adj_matrix.lean
7cfd6b2 
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
@l534zhan @kmill
Update src/combinatorics/simple_graph/adj_matrix.lean
d6cba4f 
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
@l534zhan
change
2cdd416
@leanprover-community leanprover-community deleted a comment from kmill Sep 6, 2021
kmill
kmill reviewed Sep 6, 2021
View reviewed changes
Copy link
Collaborator

@kmill kmill left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Some more comments and some shortened proofs.

src/combinatorics/simple_graph/adj_matrix.lean Show resolved Hide resolved
src/combinatorics/simple_graph/adj_matrix.lean Outdated Show resolved Hide resolved
src/combinatorics/simple_graph/adj_matrix.lean Outdated Show resolved Hide resolved
src/combinatorics/simple_graph/adj_matrix.lean Outdated Show resolved Hide resolved
src/combinatorics/simple_graph/adj_matrix.lean Show resolved Hide resolved
src/combinatorics/simple_graph/adj_matrix.lean Outdated Show resolved Hide resolved
src/combinatorics/simple_graph/adj_matrix.lean Outdated Show resolved Hide resolved
src/combinatorics/simple_graph/adj_matrix.lean Show resolved Hide resolved
src/combinatorics/simple_graph/adj_matrix.lean Outdated Show resolved Hide resolved
src/combinatorics/simple_graph/adj_matrix.lean Outdated Show resolved Hide resolved
l534zhan and others added 10 commits September 6, 2021 19:12
@l534zhan @kmill
Update src/combinatorics/simple_graph/adj_matrix.lean
d4a5320 
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
@l534zhan @kmill
Update src/combinatorics/simple_graph/adj_matrix.lean
00e4145 
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
@l534zhan @kmill
Update src/combinatorics/simple_graph/adj_matrix.lean
bd1b4cd 
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
@l534zhan @kmill
Update src/combinatorics/simple_graph/adj_matrix.lean
07badf2 
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
@l534zhan @kmill
Update src/combinatorics/simple_graph/adj_matrix.lean
7a98d93 
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
@l534zhan @kmill
Update src/combinatorics/simple_graph/adj_matrix.lean
d1adf86 
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
@l534zhan
change
afa289d
@l534zhan
Merge branch 'adj_lz' of https://github.com/leanprover-community/mathlib
b3c5e63 
 into adj_lz
@l534zhan @kmill
Update src/combinatorics/simple_graph/adj_matrix.lean
0090fe0 
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
@l534zhan
Merge branch 'adj_lz' of https://github.com/leanprover-community/mathlib
cbbdd07 
 into adj_lz
@l534zhan l534zhan requested a review from kmill September 6, 2021 18:39
@l534zhan @kmill
Update src/combinatorics/simple_graph/adj_matrix.lean
2ce2fc4 
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
@l534zhan l534zhan added the awaiting-review The author would like community review of the PR label Sep 8, 2021
@jcommelin
Copy link
Member

bors d=kmill

@bors
Copy link

bors bot commented Sep 8, 2021

✌️ kmill can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@github-actions github-actions bot added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Sep 8, 2021
@l534zhan
Copy link
Collaborator Author

l534zhan commented Sep 8, 2021

@kmill Hi, Kyle. Any further suggestions? If not, how about approving this PR?

kmill
kmill approved these changes Sep 8, 2021
View reviewed changes
Copy link
Collaborator

@kmill kmill left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think renaming loopless is the last thing I'd like to ask of you before merging. Thanks for your PR!

l534zhan and others added 2 commits September 10, 2021 18:11
@l534zhan @kmill
Update src/combinatorics/simple_graph/adj_matrix.lean
2aaa543 
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
@l534zhan
change
05a85d9
@l534zhan
Copy link
Collaborator Author

@kmill HI! I have changed accordingly! How about approving this PR now?

@l534zhan l534zhan requested a review from kmill September 10, 2021 17:13
@kmill
Copy link
Collaborator

kmill commented Sep 10, 2021 •
edited
Loading

Thanks @l534zhan 🎉

bors r+

(By the way, you usually don't need to request a review from someone more than once -- anyone who interacts with a PR gets e-mails whenever there are messages or new commits.)

bors bot pushed a commit that referenced this pull request Sep 10, 2021
@l534zhan @kmill
feat(combinatorics/simple_graph/adj_matrix): more lemmas (#9021)
400418c 


Co-authored-by: l534zhan <84618936+l534zhan@users.noreply.github.com>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
@bors
Copy link

bors bot commented Sep 10, 2021

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Sep 10, 2021
@l534zhan @kmill
feat(combinatorics/simple_graph/adj_matrix): more lemmas (#9021)
0e014ba 


Co-authored-by: l534zhan <84618936+l534zhan@users.noreply.github.com>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
@bors
Copy link

bors bot commented Sep 10, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(combinatorics/simple_graph/adj_matrix): more lemmas [Merged by Bors] - feat(combinatorics/simple_graph/adj_matrix): more lemmas Sep 10, 2021
@bors bors bot closed this Sep 10, 2021
@bors bors bot deleted the adj_lz branch September 10, 2021 20:31
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@eric-wieser eric-wieser Awaiting requested review from eric-wieser

@jcommelin jcommelin Awaiting requested review from jcommelin

@b-mehta b-mehta Awaiting requested review from b-mehta

@kmill kmill Awaiting requested review from kmill

Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@l534zhan @jcommelin @kmill @eric-wieser