Skip to content

[Merged by Bors] - feat: port LinearAlgebra.Matrix.MvPolynomial#3547

Closed
Ruben-VandeVelde wants to merge 5 commits intomasterfrom
port/LinearAlgebra.Matrix.MvPolynomial
Closed

[Merged by Bors] - feat: port LinearAlgebra.Matrix.MvPolynomial#3547
Ruben-VandeVelde wants to merge 5 commits intomasterfrom
port/LinearAlgebra.Matrix.MvPolynomial

Conversation

@Ruben-VandeVelde
Copy link
Copy Markdown
Contributor

@Ruben-VandeVelde Ruben-VandeVelde commented Apr 20, 2023 •
edited by github-actions bot
Loading

@Ruben-VandeVelde Ruben-VandeVelde added WIP Work in progress mathlib-port This is a port of a theory file from mathlib. blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) awaiting-review and removed WIP Work in progress labels Apr 20, 2023
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Apr 20, 2023

bors d+

Please merge this after bors has finished merging the dependent PR.

@bors
Copy link
Copy Markdown

bors bot commented Apr 20, 2023

✌️ Ruben-VandeVelde 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
@Ruben-VandeVelde
feat: port LinearAlgebra.Matrix.MvPolynomial
58f5d33
@Ruben-VandeVelde
Initial file copy from mathport
7143485
@Ruben-VandeVelde
automated fixes
d46c01d 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@Ruben-VandeVelde
Fix
a8a5a47
@Ruben-VandeVelde
Automated
ab343a5
@Ruben-VandeVelde Ruben-VandeVelde force-pushed the port/LinearAlgebra.Matrix.MvPolynomial branch from 4b3eb95 to ab343a5 Compare April 20, 2023 11:30
@Ruben-VandeVelde
Copy link
Copy Markdown
Contributor Author

Ruben-VandeVelde commented Apr 20, 2023

bors r+

@bors
Copy link
Copy Markdown

bors bot commented Apr 20, 2023

👎 Rejected by label

@kim-em kim-em removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Apr 20, 2023
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Apr 20, 2023

This PR/issue depends on:

@Ruben-VandeVelde
Copy link
Copy Markdown
Contributor Author

Ruben-VandeVelde commented Apr 20, 2023

bors r+

bors bot pushed a commit that referenced this pull request Apr 20, 2023
@Ruben-VandeVelde
feat: port LinearAlgebra.Matrix.MvPolynomial (#3547)
d394799
@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.Matrix.MvPolynomial [Merged by Bors] - feat: port LinearAlgebra.Matrix.MvPolynomial Apr 20, 2023
@bors bors bot closed this Apr 20, 2023
@bors bors bot deleted the port/LinearAlgebra.Matrix.MvPolynomial branch April 20, 2023 15:35
kbuzzard pushed a commit that referenced this pull request Apr 22, 2023
@Ruben-VandeVelde @kbuzzard
feat: port LinearAlgebra.Matrix.MvPolynomial (#3547)
825b97c
kim-em pushed a commit that referenced this pull request May 10, 2023
@Ruben-VandeVelde
feat: port LinearAlgebra.Matrix.MvPolynomial (#3547)
7538b6f
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

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.

2 participants

@Ruben-VandeVelde @kim-em