[Merged by Bors] - chore: small splits of RingTheory.Ideal.Operations; clean imports
#12090
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Vierkantor
added
awaiting-review
Maybe use |
Vierkantor
force-pushed
the
split-IdealOperations
branch
from
af68c57
to
2cd4fc4
Compare
Ruben-VandeVelde
approved these changes
Apr 19, 2024
|
🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde. |
1 task
|
bors merge |
github-actions
bot
added
ready-to-merge
mathlib-bors bot
pushed a commit
that referenced
this pull request
Apr 19, 2024
…12090) This is based on seeing the import `RingTheory.Ideal.Operations` → `LinearAlgebra.Basis` on the [longest pole](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/The.20long.20pole.20in.20mathlib/near/432898637). It feels like `Ideal.Operations` is a bit of a chokepoint for compiling Mathlib since it imports many files and is imported by many files. So splitting out a few obvious parts should help with compile times. Moreover, there are a bunch of imports that I could remove and have the file still compile: presumably these are (were) transitive dependencies that shake does not remove. The following results and their corollaries were split off: * `Ideal.basisSpanSingleton` * `Basis.mem_ideal_iff` * `Ideal.colon` In particular, now `Ideal.Operations` should no longer need to know about `Basis` or submodule quotients.
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
RingTheory.Ideal.Operations; clean importsRingTheory.Ideal.Operations; clean imports
mathlib-bors bot
pushed a commit
that referenced
this pull request
Apr 19, 2024
This PR was supposed to be simultaneous with #12090 but I got ill last week. This is based on seeing the import `Algebra.Algebra.Subalgebra.Basic → RingTheory.Ideal.Operations` on the [longest pole](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/The.20long.20pole.20in.20mathlib/near/432898637). It feels like `Ideal.Operations` should not be needed to define the notion of subalgebra, only to construct some interesting examples. So I removed the import and split off anything that wouldn't fit. The following results and their corollaries were split off: * `Subalgebra.prod` * `Subalgebra.iSupLift` * `AlgHom.ker_rangeRestrict` * `Subalgebra.mem_of_finset_sum_eq_one_of_pow_smul_mem` Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
mathlib-bors bot
pushed a commit
that referenced
this pull request
Apr 20, 2024
This PR was supposed to be simultaneous with #12090 but I got ill last week. This is based on seeing the import `Algebra.Algebra.Subalgebra.Basic → RingTheory.Ideal.Operations` on the [longest pole](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/The.20long.20pole.20in.20mathlib/near/432898637). It feels like `Ideal.Operations` should not be needed to define the notion of subalgebra, only to construct some interesting examples. So I removed the import and split off anything that wouldn't fit. The following results and their corollaries were split off: * `Subalgebra.prod` * `Subalgebra.iSupLift` * `AlgHom.ker_rangeRestrict` * `Subalgebra.mem_of_finset_sum_eq_one_of_pow_smul_mem` Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
callesonne
pushed a commit
that referenced
this pull request
Apr 22, 2024
…12090) This is based on seeing the import `RingTheory.Ideal.Operations` → `LinearAlgebra.Basis` on the [longest pole](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/The.20long.20pole.20in.20mathlib/near/432898637). It feels like `Ideal.Operations` is a bit of a chokepoint for compiling Mathlib since it imports many files and is imported by many files. So splitting out a few obvious parts should help with compile times. Moreover, there are a bunch of imports that I could remove and have the file still compile: presumably these are (were) transitive dependencies that shake does not remove. The following results and their corollaries were split off: * `Ideal.basisSpanSingleton` * `Basis.mem_ideal_iff` * `Ideal.colon` In particular, now `Ideal.Operations` should no longer need to know about `Basis` or submodule quotients.
callesonne
pushed a commit
that referenced
this pull request
Apr 22, 2024
This PR was supposed to be simultaneous with #12090 but I got ill last week. This is based on seeing the import `Algebra.Algebra.Subalgebra.Basic → RingTheory.Ideal.Operations` on the [longest pole](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/The.20long.20pole.20in.20mathlib/near/432898637). It feels like `Ideal.Operations` should not be needed to define the notion of subalgebra, only to construct some interesting examples. So I removed the import and split off anything that wouldn't fit. The following results and their corollaries were split off: * `Subalgebra.prod` * `Subalgebra.iSupLift` * `AlgHom.ker_rangeRestrict` * `Subalgebra.mem_of_finset_sum_eq_one_of_pow_smul_mem` Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Jun2M
pushed a commit
that referenced
this pull request
Apr 24, 2024
…12090) This is based on seeing the import `RingTheory.Ideal.Operations` → `LinearAlgebra.Basis` on the [longest pole](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/The.20long.20pole.20in.20mathlib/near/432898637). It feels like `Ideal.Operations` is a bit of a chokepoint for compiling Mathlib since it imports many files and is imported by many files. So splitting out a few obvious parts should help with compile times. Moreover, there are a bunch of imports that I could remove and have the file still compile: presumably these are (were) transitive dependencies that shake does not remove. The following results and their corollaries were split off: * `Ideal.basisSpanSingleton` * `Basis.mem_ideal_iff` * `Ideal.colon` In particular, now `Ideal.Operations` should no longer need to know about `Basis` or submodule quotients.
Jun2M
pushed a commit
that referenced
this pull request
Apr 24, 2024
This PR was supposed to be simultaneous with #12090 but I got ill last week. This is based on seeing the import `Algebra.Algebra.Subalgebra.Basic → RingTheory.Ideal.Operations` on the [longest pole](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/The.20long.20pole.20in.20mathlib/near/432898637). It feels like `Ideal.Operations` should not be needed to define the notion of subalgebra, only to construct some interesting examples. So I removed the import and split off anything that wouldn't fit. The following results and their corollaries were split off: * `Subalgebra.prod` * `Subalgebra.iSupLift` * `AlgHom.ker_rangeRestrict` * `Subalgebra.mem_of_finset_sum_eq_one_of_pow_smul_mem` Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This is based on seeing the import
RingTheory.Ideal.Operations→LinearAlgebra.Basison the longest pole. It feels likeIdeal.Operationsis a bit of a chokepoint for compiling Mathlib since it imports many files and is imported by many files. So splitting out a few obvious parts should help with compile times. Moreover, there are a bunch of imports that I could remove and have the file still compile: presumably these are (were) transitive dependencies that shake does not remove.The following results and their corollaries were split off:
Ideal.basisSpanSingletonBasis.mem_ideal_iffIdeal.colonIn particular, now
Ideal.Operationsshould no longer need to know aboutBasisor submodule quotients.