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 (Lattice/Covolume): Add results linking point counting in lattices and covolume #12488

Closed
wants to merge 42 commits into from
Closed

[Merged by Bors] - feat (Lattice/Covolume): Add results linking point counting in lattices and covolume #12488

wants to merge 42 commits into from

Conversation

xroblot
Copy link
Collaborator

@xroblot xroblot commented Apr 28, 2024 •
edited
Loading

@xroblot xroblot added WIP Work in progress t-algebra Algebra (groups, rings, fields, etc) t-measure-probability Measure theory / Probability theory and removed t-measure-probability Measure theory / Probability theory labels Apr 28, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Apr 28, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 13, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 9, 2024
@xroblot xroblot mentioned this pull request Oct 19, 2024
Open
13 tasks
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 21, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 24, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 30, 2024
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Dec 5, 2024
@mathlib4-dependent-issues-bot
Copy link
Collaborator

This PR/issue depends on:

@xroblot xroblot added the WIP Work in progress label Dec 5, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 5, 2024
@xroblot xroblot removed the WIP Work in progress label Dec 13, 2024
@riccardobrasca riccardobrasca self-assigned this Dec 16, 2024
riccardobrasca
riccardobrasca approved these changes Dec 17, 2024
View reviewed changes
Copy link
Member

@riccardobrasca riccardobrasca left a comment

Choose a reason for hiding this comment

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

Thanks!

bors d+

Mathlib/Algebra/Module/ZLattice/Covolume.lean Outdated Show resolved Hide resolved
Mathlib/Algebra/Module/ZLattice/Covolume.lean Show resolved Hide resolved
Mathlib/LinearAlgebra/Determinant.lean Show resolved Hide resolved
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Dec 17, 2024

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

@xroblot
Copy link
Collaborator Author

xroblot commented Dec 18, 2024

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Dec 18, 2024
@xroblot
feat (Lattice/Covolume): Add results linking point counting in lattic…
211dc53 
…es and covolume (#12488)

Co-authored-by: Xavier Roblot <46200072+xroblot@users.noreply.github.com>
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Dec 18, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat (Lattice/Covolume): Add results linking point counting in lattices and covolume [Merged by Bors] - feat (Lattice/Covolume): Add results linking point counting in lattices and covolume Dec 18, 2024
@mathlib-bors mathlib-bors bot closed this Dec 18, 2024
@mathlib-bors mathlib-bors bot deleted the xfr-pointcounting branch December 18, 2024 16:02
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@riccardobrasca riccardobrasca riccardobrasca approved these changes

Assignees

@riccardobrasca riccardobrasca

Labels
delegated t-algebra Algebra (groups, rings, fields, etc)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
6 participants
@xroblot @mathlib4-dependent-issues-bot @riccardobrasca @YaelDillies @leanprover-community-bot-assistant @leanprover-community-mathlib4-bot