Skip to content

[Merged by Bors] - feat(LinearAlgebra/TensorProduct/Subalgebra): some linear maps induced by multiplication for subalgebras#14611

Closed
acmepjz wants to merge 3 commits intomasterfrom
acmepjz_mulmap_subalg
Closed

[Merged by Bors] - feat(LinearAlgebra/TensorProduct/Subalgebra): some linear maps induced by multiplication for subalgebras#14611
acmepjz wants to merge 3 commits intomasterfrom
acmepjz_mulmap_subalg

Conversation

@acmepjz
Copy link
Copy Markdown
Collaborator

@acmepjz acmepjz commented Jul 10, 2024

This is the follow-up of the PR #12498. It is used in the definition of linearly disjointness (#9651).

Open in Gitpod

@acmepjz acmepjz added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-algebra Algebra (groups, rings, fields, etc) labels Jul 10, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jul 10, 2024 •
edited
Loading

PR summary a408bb210d

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.LinearAlgebra.TensorProduct.Subalgebra 1157

Declarations diff

+ comm_trans_lTensorBot
+ comm_trans_rTensorBot
+ finrank_sup_le_of_free
+ lTensorBot
+ lTensorBot_one_tmul
+ lTensorBot_symm_apply
+ lTensorBot_tmul
+ mulMap
+ mulMap'
+ mulMap'_surjective
+ mulMap_bot_left_eq
+ mulMap_bot_right_eq
+ mulMap_comm
+ mulMap_range
+ mulMap_tmul
+ mulMap_toLinearMap
+ rTensorBot
+ rTensorBot_symm_apply
+ rTensorBot_tmul
+ rTensorBot_tmul_one
+ rank_sup_le_of_free
+ val_mulMap'_tmul

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jul 10, 2024
@eric-wieser eric-wieser added the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 11, 2024
@acmepjz acmepjz removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 11, 2024
@erdOne
Copy link
Copy Markdown
Member

erdOne commented Jul 16, 2024

Thanks!
maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jul 16, 2024

🚀 Pull request has been placed on the maintainer queue by erdOne.

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jul 16, 2024
jcommelin
jcommelin reviewed Jul 16, 2024
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks 🎉

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Jul 16, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jul 16, 2024
@acmepjz
feat(LinearAlgebra/TensorProduct/Subalgebra): some linear maps induce…
335d975 
…d by multiplication for subalgebras (#14611)

This is the follow-up of the PR #12498. It is used in the definition of linearly disjointness (#9651).
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jul 16, 2024

Build failed (retrying...):

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jul 16, 2024

✌️ acmepjz can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jul 16, 2024

Canceled.

@acmepjz
Copy link
Copy Markdown
Collaborator Author

acmepjz commented Jul 16, 2024

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Jul 16, 2024
@acmepjz
feat(LinearAlgebra/TensorProduct/Subalgebra): some linear maps induce…
6f640f8 
…d by multiplication for subalgebras (#14611)

This is the follow-up of the PR #12498. It is used in the definition of linearly disjointness (#9651).
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jul 16, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(LinearAlgebra/TensorProduct/Subalgebra): some linear maps induced by multiplication for subalgebras [Merged by Bors] - feat(LinearAlgebra/TensorProduct/Subalgebra): some linear maps induced by multiplication for subalgebras Jul 16, 2024
@mathlib-bors mathlib-bors bot closed this Jul 16, 2024
@mathlib-bors mathlib-bors bot deleted the acmepjz_mulmap_subalg branch July 16, 2024 22:43
@adomani adomani mentioned this pull request Aug 1, 2024
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

@jcommelin jcommelin jcommelin left review comments

Assignees

No one assigned

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@acmepjz @erdOne @eric-wieser @jcommelin