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.
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
[Merged by Bors] - chore: Reorganize results about rank
and finrank
.
#9349
Conversation
…r-community/mathlib4 into erd1/refactorDimension
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks a lot for this effort 🎉
Two minor comments.
bors d+
✌️ erdOne can now approve this pull request. To approve and merge a pull request, simply reply with |
…lib4 into erd1/refactorDimension
bors merge |
Canceled. |
bors merge |
The files `Mathlib.LinearAlgebra.FreeModule.Rank`, `Mathlib.LinearAlgebra.FreeModule.Finite.Rank`, `Mathlib.LinearAlgebra.Dimension` and `Mathlib.LinearAlgebra.Finrank` were reorganized into a folder `Mathlib.LinearAlgebra.Dimension`, containing the following files - `Basic.lean`: Contains the definition of `Module.rank`. - `Finrank.lean`: Contains the definition of `FiniteDimensional.finrank`. - `StrongRankCondition.lean`: Contains results about `rank` and `finrank` over rings satisfying strong rank condition - `Free.lean`: Contains results about `rank` and `finrank` of free modules - `Finite.lean`: Contains conditions or consequences for `rank` to be finite or zero - `Constructions.lean`: Contains the calculation of the `rank` of various constructions. - `DivisionRing.lean`: Contains results about `rank` and `finrank` of spaces over division rings. - `LinearMap.lean`: Contains results about `LinearMap.rank` API changes: `IsNoetherian.rank_lt_aleph0` and `FiniteDimensional.rank_lt_aleph0` are replaced with `rank_lt_aleph0`. `Module.Free.finite_basis` was renamed to `Module.Finite.finite_basis`. `FiniteDimensional.finrank_eq_rank` was renamed to `finrank_eq_rank`. `rank_eq_cardinal_basis` and `rank_eq_cardinal_basis'` were removed in favour of `Basis.mk_eq_mk` and `Basis.mk_eq_mk''`. Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded! And happy new year! 🎉 |
rank
and finrank
.rank
and finrank
.
The files
Mathlib.LinearAlgebra.FreeModule.Rank
,Mathlib.LinearAlgebra.FreeModule.Finite.Rank
,Mathlib.LinearAlgebra.Dimension
andMathlib.LinearAlgebra.Finrank
were reorganized into afolder
Mathlib.LinearAlgebra.Dimension
, containing the following filesBasic.lean
: Contains the definition ofModule.rank
.Finrank.lean
: Contains the definition ofFiniteDimensional.finrank
.StrongRankCondition.lean
: Contains results aboutrank
andfinrank
over rings satisfying strong rank condition
Free.lean
: Contains results aboutrank
andfinrank
of free modulesFinite.lean
: Contains conditions or consequences forrank
to be finite or zeroConstructions.lean
: Contains the calculation of therank
of various constructions.DivisionRing.lean
: Contains results aboutrank
andfinrank
of spaces over division rings.LinearMap.lean
: Contains results aboutLinearMap.rank
API changes:
IsNoetherian.rank_lt_aleph0
andFiniteDimensional.rank_lt_aleph0
are replaced withrank_lt_aleph0
.Module.Free.finite_basis
was renamed toModule.Finite.finite_basis
.FiniteDimensional.finrank_eq_rank
was renamed tofinrank_eq_rank
.rank_eq_cardinal_basis
andrank_eq_cardinal_basis'
were removedin favour of
Basis.mk_eq_mk
andBasis.mk_eq_mk''
.