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

[Merged by Bors] - feat(order/modular_lattice): Semimodular lattices#11602

Closed
YaelDillies wants to merge 6 commits into
masterfrom
semimodular_lattice
Closed

[Merged by Bors] - feat(order/modular_lattice): Semimodular lattices#11602
YaelDillies wants to merge 6 commits into
masterfrom
semimodular_lattice

Conversation

@YaelDillies

Copy link
Copy Markdown
Collaborator

This defines the four main kinds of semimodular lattices:

  • Weakly upper modular
  • Weakly lower modular
  • Upper modular
  • Lower modular

Open in Gitpod

@YaelDillies YaelDillies added the awaiting-review The author would like community review of the PR label Jan 22, 2022

@jcommelin jcommelin left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

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

Modulo naming: lgtm.

Comment thread src/order/modular_lattice.lean Outdated
@jcommelin jcommelin added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Jan 26, 2022
@rwbarton

Copy link
Copy Markdown
Collaborator

Can you add a reference?

@YaelDillies YaelDillies added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Feb 12, 2022
Comment thread src/order/modular_lattice.lean Outdated
@ocfnash

ocfnash commented Feb 21, 2022

Copy link
Copy Markdown
Collaborator

Can you add a reference?

I see you did add a reference but only to Wikipedia. If that's all there is then fine, but it would be great if there was an academic reference.

@ocfnash

ocfnash commented Feb 21, 2022

Copy link
Copy Markdown
Collaborator

Also, naming aside, this LGTM.

@ocfnash ocfnash added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Feb 21, 2022
@YaelDillies YaelDillies added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jun 27, 2022
@YaelDillies

Copy link
Copy Markdown
Collaborator Author

I do not have a better reference unfortunately. But maybe @apnelson1 does?

@apnelson1

Copy link
Copy Markdown
Collaborator

I would go with this one:

Stern, M. (1999). Semimodular Lattices: Theory and Applications (Encyclopedia of Mathematics and its Applications). Cambridge: Cambridge University Press. doi:10.1017/CBO9780511665578

@jcommelin jcommelin left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@leanprover-community-bot-assistant leanprover-community-bot-assistant added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Jul 11, 2022
bors Bot pushed a commit that referenced this pull request Jul 11, 2022
This defines the four main kinds of semimodular lattices:
* Weakly upper modular
* Weakly lower modular
* Upper modular
* Lower modular
@bors

bors Bot commented Jul 11, 2022

Copy link
Copy Markdown

Build failed (retrying...):

@urkud

urkud commented Jul 11, 2022

Copy link
Copy Markdown
Member

I'll add it back to queue in a minute.
bors r-

@bors

bors Bot commented Jul 11, 2022

Copy link
Copy Markdown

Canceled.

@urkud

urkud commented Jul 11, 2022

Copy link
Copy Markdown
Member

bors r+

bors Bot pushed a commit that referenced this pull request Jul 11, 2022
This defines the four main kinds of semimodular lattices:
* Weakly upper modular
* Weakly lower modular
* Upper modular
* Lower modular
@bors

bors Bot commented Jul 11, 2022

Copy link
Copy Markdown

Pull request successfully merged into master.

Build succeeded:

@bors bors Bot changed the title feat(order/modular_lattice): Semimodular lattices [Merged by Bors] - feat(order/modular_lattice): Semimodular lattices Jul 11, 2022
@bors bors Bot closed this Jul 11, 2022
@bors
bors Bot deleted the semimodular_lattice branch July 11, 2022 19:17
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Labels

ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

7 participants