[Merged by Bors] - chore(Algebra/Algebra): split Subalgebra.Basic
#12267
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
Ruben-VandeVelde
approved these changes
Apr 19, 2024
Indeed! The motivation is slightly different, though: this PR is more about cleaning up the import graph, between files, and that change would be more about cleaning up the declaration list within the file. |
The main purpose of this refactor is to remove the dependency of `Algebra.Subalgebra.Basic` (which is imported in quite a few places) on the heavy import `RingTheory.Ideal.Operations`.
leanprover-community-mathlib4-bot
added
the
merge-conflict
Vierkantor
force-pushed
the
split-SubalgebraBasic
branch
from
423a036
to
f5d2f03
Compare
leanprover-community-mathlib4-bot
removed
the
merge-conflict
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
|
maintainer merge |
|
🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde. |
|
Thanks 🎉 bors merge |
github-actions
bot
added
ready-to-merge
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>
|
Build failed: |
|
bors r+ |
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>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
Subalgebra.BasicSubalgebra.Basic
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
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 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.Operationson the longest pole. It feels likeIdeal.Operationsshould 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.prodSubalgebra.iSupLiftAlgHom.ker_rangeRestrictSubalgebra.mem_of_finset_sum_eq_one_of_pow_smul_mem