Skip to content

[Merged by Bors] - feat: port LinearAlgebra.FreeModule.PID#3434

Closed
xroblot wants to merge 19 commits intomasterfrom
port/LinearAlgebra.FreeModule.Pid
Closed

[Merged by Bors] - feat: port LinearAlgebra.FreeModule.PID#3434
xroblot wants to merge 19 commits intomasterfrom
port/LinearAlgebra.FreeModule.Pid

Conversation

@xroblot
Copy link
Copy Markdown
Collaborator

@xroblot xroblot commented Apr 14, 2023

Open in Gitpod

xroblot added 3 commits April 14, 2023 09:15
@xroblot
feat: port LinearAlgebra.FreeModule.Pid
a0eba45
@xroblot
Initial file copy from mathport
2c1dd65
@xroblot
automated fixes
20fb08d 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@xroblot xroblot added WIP Work in progress mathlib-port This is a port of a theory file from mathlib. labels Apr 14, 2023
@kim-em kim-em added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 14, 2023
@kim-em kim-em removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 18, 2023
@Parcly-Taxel Parcly-Taxel changed the title feat: port LinearAlgebra.FreeModule.Pid feat: port LinearAlgebra.FreeModule.PID Apr 20, 2023
@Parcly-Taxel Parcly-Taxel added awaiting-review and removed WIP Work in progress labels Apr 20, 2023
kim-em
kim-em reviewed Apr 20, 2023
View reviewed changes
kim-em
kim-em reviewed Apr 20, 2023
View reviewed changes
kim-em
kim-em reviewed Apr 20, 2023
View reviewed changes
kim-em
kim-em reviewed Apr 20, 2023
View reviewed changes
kim-em
kim-em reviewed Apr 20, 2023
View reviewed changes
@kim-em kim-em added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Apr 20, 2023
@xroblot xroblot added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Apr 20, 2023
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Apr 20, 2023

bors d+

@bors
Copy link
Copy Markdown

bors bot commented Apr 20, 2023

✌️ 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 This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Apr 20, 2023
@xroblot
Copy link
Copy Markdown
Collaborator Author

xroblot commented Apr 20, 2023

bors r+

bors bot pushed a commit that referenced this pull request Apr 20, 2023
@xroblot @Parcly-Taxel
feat: port LinearAlgebra.FreeModule.PID (#3434)
a0ec959 
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Apr 20, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port LinearAlgebra.FreeModule.PID [Merged by Bors] - feat: port LinearAlgebra.FreeModule.PID Apr 20, 2023
@bors bors bot closed this Apr 20, 2023
@bors bors bot deleted the port/LinearAlgebra.FreeModule.Pid branch April 20, 2023 12:30
kbuzzard pushed a commit that referenced this pull request Apr 22, 2023
@xroblot @Parcly-Taxel @kbuzzard
feat: port LinearAlgebra.FreeModule.PID (#3434)
433ba2a 
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
kim-em pushed a commit that referenced this pull request May 10, 2023
@xroblot @Parcly-Taxel
feat: port LinearAlgebra.FreeModule.PID (#3434)
833f676 
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kim-em kim-em kim-em left review comments

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). mathlib-port This is a port of a theory file from mathlib.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@xroblot @kim-em @Parcly-Taxel