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] - chore: Define the class IsZlattice #11356

Closed
wants to merge 12 commits into from
Closed

[Merged by Bors] - chore: Define the class IsZlattice #11356

wants to merge 12 commits into from

Conversation

xroblot
Copy link
Collaborator

@xroblot xroblot commented Mar 13, 2024 •
edited
Loading

See the Zulip thread

Open in Gitpod

@xroblot xroblot added WIP Work in progress t-algebra Algebra (groups, rings, fields etc) labels Mar 13, 2024
@xroblot
Copy link
Collaborator Author

xroblot commented Mar 13, 2024

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 1936fcd.
The entire run failed.
Found no significant differences.

@xroblot
Copy link
Collaborator Author

xroblot commented Mar 13, 2024

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 1406074.
There were no significant changes against commit 526c94c.

@xroblot xroblot added awaiting-review and removed WIP Work in progress labels Mar 13, 2024
@xroblot xroblot added WIP Work in progress and removed awaiting-review labels Mar 13, 2024
@riccardobrasca riccardobrasca self-assigned this Mar 13, 2024
@xroblot xroblot added awaiting-review and removed WIP Work in progress labels Mar 14, 2024
@sgouezel sgouezel added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review labels Mar 14, 2024
@xroblot xroblot removed the awaiting-author A reviewer has asked the author a question or requested changes label Mar 16, 2024
@riccardobrasca
Copy link
Member

Can you add a TODO explaining that sooner or later we want a version not over Z? Thanks!

bors d+

@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Mar 18, 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 Mar 18, 2024

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Mar 18, 2024
@xroblot
chore: Define the class IsZlattice (#11356)
6aee244 
See the Zulip [thread](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Class.20.60IsZlattice.60/near/426301607)
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Mar 18, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: Define the class IsZlattice [Merged by Bors] - chore: Define the class IsZlattice Mar 18, 2024
@mathlib-bors mathlib-bors bot closed this Mar 18, 2024
@mathlib-bors mathlib-bors bot deleted the xfr_zlattice_class branch March 18, 2024 13:06
dagurtomas pushed a commit that referenced this pull request Mar 22, 2024
@xroblot @dagurtomas
chore: Define the class IsZlattice (#11356)
6ba1a74 
See the Zulip [thread](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Class.20.60IsZlattice.60/near/426301607)
utensil pushed a commit that referenced this pull request Mar 26, 2024
@xroblot @utensil
chore: Define the class IsZlattice (#11356)
50b60c3 
See the Zulip [thread](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Class.20.60IsZlattice.60/near/426301607)
Louddy pushed a commit that referenced this pull request Apr 15, 2024
@xroblot @Louddy
chore: Define the class IsZlattice (#11356)
f7d274e 
See the Zulip [thread](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Class.20.60IsZlattice.60/near/426301607)
atarnoam pushed a commit that referenced this pull request Apr 16, 2024
@xroblot @atarnoam
chore: Define the class IsZlattice (#11356)
c357082 
See the Zulip [thread](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Class.20.60IsZlattice.60/near/426301607)
uniwuni pushed a commit that referenced this pull request Apr 19, 2024
@xroblot @uniwuni
chore: Define the class IsZlattice (#11356)
e481cf3 
See the Zulip [thread](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Class.20.60IsZlattice.60/near/426301607)
callesonne pushed a commit that referenced this pull request Apr 22, 2024
@xroblot @callesonne
chore: Define the class IsZlattice (#11356)
8023188 
See the Zulip [thread](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Class.20.60IsZlattice.60/near/426301607)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@sgouezel sgouezel sgouezel left review comments

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.

None yet
4 participants
@xroblot @leanprover-bot @riccardobrasca @sgouezel