Skip to content
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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat: port LinearAlgebra.TensorProductBasis #3295

Closed
wants to merge 6 commits into from
Closed

[Merged by Bors] - feat: port LinearAlgebra.TensorProductBasis #3295

wants to merge 6 commits into from

Conversation

mattrobball
Copy link
Collaborator

@mattrobball mattrobball commented Apr 6, 2023 •
edited by github-actions bot

@mattrobball
feat: port LinearAlgebra.TensorProductBasis
905f8b4
@mattrobball
Initial file copy from mathport
ae388f3
@mattrobball
automated fixes
4fe3b82 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@mattrobball
Squashed commit of the following:
48305a3 
commit 1387eab
Author: Matthew Ballard <matt@mrb.email>
Date:   Wed Apr 5 23:17:06 2023 -0400

    fix errors

commit c413bb6
Merge: 1827e0a f1501f9
Author: Matthew Ballard <matt@mrb.email>
Date:   Wed Apr 5 22:05:16 2023 -0400

    Merge remote-tracking branch 'origin/port/LinearAlgebra.StdBasis' into port/LinearAlgebra.FinsuppVectorSpace

commit 1827e0a
Author: Matthew Ballard <matt@mrb.email>
Date:   Wed Apr 5 22:04:51 2023 -0400

    automated fixes

    Mathbin -> Mathlib
    fix certain import statements
    move "by" to end of line
    add import to Mathlib.lean

commit 39c3d27
Author: Matthew Ballard <matt@mrb.email>
Date:   Wed Apr 5 22:04:51 2023 -0400

    Initial file copy from mathport

commit 10a8e45
Author: Matthew Ballard <matt@mrb.email>
Date:   Wed Apr 5 22:04:51 2023 -0400

    feat: port LinearAlgebra.FinsuppVectorSpace

commit f1501f9
Author: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Date:   Thu Apr 6 00:40:28 2023 +0800

    Lint?

commit 9aa757d
Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date:   Wed Apr 5 18:19:30 2023 +0200

    Warnings

commit 5ff0c94
Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date:   Wed Apr 5 18:18:02 2023 +0200

    Automated

commit 3bb0bde
Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date:   Wed Apr 5 18:17:00 2023 +0200

    Typo

commit 11f9ae5
Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date:   Wed Apr 5 18:15:47 2023 +0200

    Warnings

commit e4d1b30
Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date:   Wed Apr 5 18:15:27 2023 +0200

    Fix

commit bfe71f0
Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date:   Wed Apr 5 18:12:54 2023 +0200

    Workaround

commit 2f5b7f9
Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date:   Wed Apr 5 18:00:00 2023 +0200

    Fix

commit 3f8249e
Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date:   Wed Apr 5 17:46:49 2023 +0200

    Fix

commit 8e0078f
Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date:   Wed Apr 5 17:37:31 2023 +0200

    Remove lean3 workaround

commit 3428b52
Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date:   Tue Apr 4 18:21:05 2023 +0200

    Partial fix

commit 8a62488
Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date:   Tue Apr 4 16:03:33 2023 +0200

    Partial fix

commit cf213ce
Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date:   Tue Apr 4 15:56:23 2023 +0200

    Partial fix

commit 46f616d
Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date:   Tue Apr 4 15:27:30 2023 +0200

    automated fixes

    Mathbin -> Mathlib
    fix certain import statements
    move "by" to end of line
    add import to Mathlib.lean

commit cb64de9
Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date:   Tue Apr 4 15:27:30 2023 +0200

    Initial file copy from mathport

commit c810965
Author: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date:   Tue Apr 4 15:27:30 2023 +0200

    feat: port LinearAlgebra.StdBasis
@mattrobball
fix errors; lint; align names
82c7b05
@mattrobball mattrobball added mathlib-port This is a port of a theory file from mathlib. awaiting-review The author would like community review of the PR labels Apr 6, 2023
@semorrison semorrison added blocked-by-other-PR This PR depends on another PR which is still in the queue. merge-conflict The PR has a merge conflict with master, and needs manual merging. labels Apr 6, 2023
@mattrobball mattrobball mentioned this pull request Apr 6, 2023
Closed
1 task
@semorrison semorrison removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Apr 7, 2023
@mattrobball mattrobball force-pushed the port/LinearAlgebra.TensorProductBasis branch from c5c4bc1 to 42e6957 Compare April 7, 2023 10:57
@mattrobball mattrobball removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. label Apr 7, 2023
@semorrison
Copy link
Contributor

This PR/issue depends on:

@ChrisHughes24
Copy link
Member

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Apr 7, 2023
bors bot pushed a commit that referenced this pull request Apr 7, 2023
@mattrobball
feat: port LinearAlgebra.TensorProductBasis (#3295)
934f05d
@bors
Copy link

bors bot commented Apr 7, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port LinearAlgebra.TensorProductBasis [Merged by Bors] - feat: port LinearAlgebra.TensorProductBasis Apr 7, 2023
@bors bors bot closed this Apr 7, 2023
@bors bors bot deleted the port/LinearAlgebra.TensorProductBasis branch April 7, 2023 11:35
MonadMaverick pushed a commit that referenced this pull request Apr 9, 2023
@mattrobball @MonadMaverick
feat: port LinearAlgebra.TensorProductBasis (#3295)
3c254ac
MonadMaverick pushed a commit that referenced this pull request Apr 9, 2023
@mattrobball @MonadMaverick
feat: port LinearAlgebra.TensorProductBasis (#3295)
b143f7b
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
mathlib-port This is a port of a theory file from mathlib. ready-to-merge This PR has been sent to bors.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@mattrobball @semorrison @ChrisHughes24