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: Split RingTheory.FractionalIdeal.Basic #9854

Closed
wants to merge 6 commits into from
Closed

[Merged by Bors] - chore: Split RingTheory.FractionalIdeal.Basic #9854

wants to merge 6 commits into from

Conversation

xroblot
Copy link
Collaborator

@xroblot xroblot commented Jan 19, 2024 •
edited

The file RingTheory.FractionalIdeal.Basic is more than 1600 lines long. This PR splits it into two files: Basic and Operations following the model of RingTheory.Ideal.Basic and RingTheory.Ideal.Operations

Open in Gitpod

@xroblot xroblot added awaiting-review The author would like community review of the PR t-algebra Algebra (groups, rings, fields etc) labels Jan 19, 2024
@riccardobrasca
Copy link
Member

Should we wait a couple of hours and merge the other PR before splitting?

@xroblot
Copy link
Collaborator Author

xroblot commented Jan 19, 2024

Should we wait a couple of hours and merge the other PR before splitting?

Let's merge this one first and then I'll fix the other one and merge it.

@riccardobrasca
Copy link
Member

Can you describe the splitting in the PR description?

@riccardobrasca
Copy link
Member

bors d+

@mathlib-bors
Copy link

mathlib-bors bot commented Jan 19, 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.

@github-actions github-actions bot added delegated and removed awaiting-review The author would like community review of the PR labels Jan 19, 2024
@xroblot
Copy link
Collaborator Author

xroblot commented Jan 19, 2024

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Jan 19, 2024
@xroblot
chore: Split RingTheory.FractionalIdeal.Basic (#9854)
17aca4e 
The file `RingTheory.FractionalIdeal.Basic` is more than 1600 lines long. This PR splits it into two files: `Basic` and `Operations` following the model of `RingTheory.Ideal.Basic` and `RingTheory.Ideal.Operations`
@mathlib-bors
Copy link

mathlib-bors bot commented Jan 19, 2024

Build failed:

@xroblot
Copy link
Collaborator Author

xroblot commented Jan 19, 2024 •
edited

Damn, it's the leantar bug

error: /home/lean/.cache/mathlib/e3fcbaaf6ab40bbf.ltar: failed to fill whole buffer
uncaught exception: leantar failed with error code 1

digama0 and others added 3 commits January 19, 2024 17:13
@digama0 @riccardobrasca
chore: reduce imports (#9830)
c2d5107 
This uses the improved `shake` script from #9772 to reduce imports across mathlib. The corresponding `noshake.json` file has been added to #9772.



Co-authored-by: Mario Carneiro <di.gama@gmail.com>
@acmepjz @riccardobrasca
feat(LinearAlgebra/LinearIndependent): add `linearIndependent_iff_fin…
5f1151c 
…set_linearIndependent` (#9797)

A family is linearly independent if and only if all of its finite subfamily is linearly independent.
@acmepjz @alreadydone @riccardobrasca
feat(FieldTheory/IsAlgClosed/Basic): add IsAlgClosed.perfectField i…
07a9af9 
…nstance (#9710)

Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
@riccardobrasca riccardobrasca added the auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. label Jan 19, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

As this PR is labelled auto-merge-after-CI, we are now sending it to bors:

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Jan 19, 2024
@xroblot @digama0 @acmepjz
chore: Split RingTheory.FractionalIdeal.Basic (#9854)
de9c7b5 
The file `RingTheory.FractionalIdeal.Basic` is more than 1600 lines long. This PR splits it into two files: `Basic` and `Operations` following the model of `RingTheory.Ideal.Basic` and `RingTheory.Ideal.Operations`

 

Co-authored-by: Mario Carneiro <mcarneir@andrew.cmu.edu>
Co-authored-by: Jz Pan <acme_pjz@hotmail.com>
@mathlib-bors
Copy link

mathlib-bors bot commented Jan 19, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: Split RingTheory.FractionalIdeal.Basic [Merged by Bors] - chore: Split RingTheory.FractionalIdeal.Basic Jan 19, 2024
@mathlib-bors mathlib-bors bot closed this Jan 19, 2024
@mathlib-bors mathlib-bors bot deleted the xfr-split_factideal_basic branch January 19, 2024 17:09
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@riccardobrasca riccardobrasca Awaiting requested review from riccardobrasca

Assignees
No one assigned
Labels
auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. 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
5 participants
@xroblot @riccardobrasca @leanprover-community-mathlib4-bot @digama0 @acmepjz