[Merged by Bors] - feat(LinearAlgebra/FiniteDimensional): relax condition of results regarding subalgebra = bot#12849
Closed
[Merged by Bors] - feat(LinearAlgebra/FiniteDimensional): relax condition of results regarding subalgebra = bot#12849
Conversation
14 tasks
Collaborator
Author
|
Seems that a lot of results in this file can be relaxed by the same way. Maybe I'll investigate them later. It's welcomed if someone could compile a list of them. |
eric-wieser
reviewed
May 12, 2024
Subalgebra.eq_bot_of_finrank_oneSubalgebra.eq_bot_of_finrank_one
Subalgebra.eq_bot_of_finrank_one
Collaborator
Author
|
Since #12963 is merged, is it a good idea to move the results in this PR to that file? |
erdOne
reviewed
May 22, 2024
Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean
Outdated
Show resolved
Hide resolved
Member
|
Thanks! |
|
🚀 Pull request has been placed on the maintainer queue by erdOne. |
Contributor
|
✌️ acmepjz can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
Collaborator
Author
|
bors r+ |
mathlib-bors bot
pushed a commit
that referenced
this pull request
May 24, 2024
…arding subalgebra = bot (#12849) ... from requiring `F` being a field to `F` satisfying `StrongRankCondition` and `S` being a free `F`-module. This makes the original statement a special case. The changed results are: `Subalgebra.eq_bot_of_(rank_le|finrank)_one`, `Subalgebra.[fin]rank_eq_one_iff` and `Subalgebra.bot_eq_top_iff_[fin]rank_eq_one`. Since the generalized results don't requiring division ring anymore, they are moved to an eariler file `LinearAlgebra/Dimension/FreeAndStrongRankCondition`. The proof need to use a new result `bijective_algebraMap_of_linearEquiv` which is put into `Algebra/Algebra/Basic`.
Contributor
|
Pull request successfully merged into master. Build succeeded: |
grunweg
pushed a commit
that referenced
this pull request
May 24, 2024
…arding subalgebra = bot (#12849) ... from requiring `F` being a field to `F` satisfying `StrongRankCondition` and `S` being a free `F`-module. This makes the original statement a special case. The changed results are: `Subalgebra.eq_bot_of_(rank_le|finrank)_one`, `Subalgebra.[fin]rank_eq_one_iff` and `Subalgebra.bot_eq_top_iff_[fin]rank_eq_one`. Since the generalized results don't requiring division ring anymore, they are moved to an eariler file `LinearAlgebra/Dimension/FreeAndStrongRankCondition`. The proof need to use a new result `bijective_algebraMap_of_linearEquiv` which is put into `Algebra/Algebra/Basic`.
callesonne
pushed a commit
that referenced
this pull request
Jun 4, 2024
…arding subalgebra = bot (#12849) ... from requiring `F` being a field to `F` satisfying `StrongRankCondition` and `S` being a free `F`-module. This makes the original statement a special case. The changed results are: `Subalgebra.eq_bot_of_(rank_le|finrank)_one`, `Subalgebra.[fin]rank_eq_one_iff` and `Subalgebra.bot_eq_top_iff_[fin]rank_eq_one`. Since the generalized results don't requiring division ring anymore, they are moved to an eariler file `LinearAlgebra/Dimension/FreeAndStrongRankCondition`. The proof need to use a new result `bijective_algebraMap_of_linearEquiv` which is put into `Algebra/Algebra/Basic`.
js2357
pushed a commit
that referenced
this pull request
Jun 18, 2024
…arding subalgebra = bot (#12849) ... from requiring `F` being a field to `F` satisfying `StrongRankCondition` and `S` being a free `F`-module. This makes the original statement a special case. The changed results are: `Subalgebra.eq_bot_of_(rank_le|finrank)_one`, `Subalgebra.[fin]rank_eq_one_iff` and `Subalgebra.bot_eq_top_iff_[fin]rank_eq_one`. Since the generalized results don't requiring division ring anymore, they are moved to an eariler file `LinearAlgebra/Dimension/FreeAndStrongRankCondition`. The proof need to use a new result `bijective_algebraMap_of_linearEquiv` which is put into `Algebra/Algebra/Basic`.
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
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.
... from requiring
Fbeing a field toFsatisfyingStrongRankConditionandSbeing a freeF-module. This makes the original statement a special case.The changed results are:
Subalgebra.eq_bot_of_(rank_le|finrank)_one,Subalgebra.[fin]rank_eq_one_iffandSubalgebra.bot_eq_top_iff_[fin]rank_eq_one.Since the generalized results don't requiring division ring anymore, they are moved to an eariler file
LinearAlgebra/Dimension/FreeAndStrongRankCondition.The proof need to use a new result
bijective_algebraMap_of_linearEquivwhich is put intoAlgebra/Algebra/Basic.discussion: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2312849.20relax.20condition.20of.20Subalgebra.2Eeq_bot_of_finrank_one