Skip to content

[Merged by Bors] - refactor(LinearAlgebra/BilinearMap): Left composition, bilinear over different rings#13042

Closed
mans0954 wants to merge 7 commits intomasterfrom
mans0954/BilinearMap-compl
Closed

[Merged by Bors] - refactor(LinearAlgebra/BilinearMap): Left composition, bilinear over different rings#13042
mans0954 wants to merge 7 commits intomasterfrom
mans0954/BilinearMap-compl

Conversation

@mans0954
Copy link
Copy Markdown
Collaborator

@mans0954 mans0954 commented May 19, 2024

Generalise compl₂ and compl₁₂ for left composition with maps which are linear over different rings in the first and second variable.

Needed for #9334

Open in Gitpod

@mans0954 mans0954 mentioned this pull request May 19, 2024
Closed
2 tasks
@mans0954 mans0954 changed the title refact(LinearAlgebra/BilinearMap): Left composition, bilinear over different rings refactor(LinearAlgebra/BilinearMap): Left composition, bilinear over different rings May 19, 2024
@mans0954 mans0954 added awaiting-review t-algebra Algebra (groups, rings, fields, etc) labels May 19, 2024
@mans0954
Copy link
Copy Markdown
Collaborator Author

mans0954 commented May 19, 2024

!bench

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented May 19, 2024

Here are the benchmark results for commit d7460b6.
There were no significant changes against commit 91e688b.

@mans0954
Copy link
Copy Markdown
Collaborator Author

mans0954 commented Jun 1, 2024

@eric-wieser do you have a moment to review this PR please? It's quite a small one.

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 7, 2024

Import summary

No significant changes to the import graph

eric-wieser
eric-wieser approved these changes Jun 8, 2024
View reviewed changes
Copy link
Copy Markdown
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

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

bors d+

The variables are getting a bit unmanageable here, but I don't have any suggestions to clean them up. Just some whitespace suggestions.

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 8, 2024

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

@ghost ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Jun 8, 2024
mans0954 and others added 2 commits June 8, 2024 21:55
@mans0954 @eric-wieser
Update Mathlib/LinearAlgebra/BilinearMap.lean
eb8dd66 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@mans0954 @eric-wieser
Update Mathlib/LinearAlgebra/BilinearMap.lean
62001e7 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 8, 2024 •
edited
Loading

PR summary

Import changes

No significant changes to the import graph

Declarations diff

No declarations were harmed in the making of this PR! 🐙

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

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

@mans0954
Copy link
Copy Markdown
Collaborator Author

mans0954 commented Jun 8, 2024

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Jun 8, 2024
@mans0954
refactor(LinearAlgebra/BilinearMap): Left composition, bilinear over …
5ddf243 
…different rings (#13042)

Generalise `compl₂` and `compl₁₂` for left composition with maps which are linear over different rings in the first and second variable.

Needed for #9334



Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 8, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title refactor(LinearAlgebra/BilinearMap): Left composition, bilinear over different rings [Merged by Bors] - refactor(LinearAlgebra/BilinearMap): Left composition, bilinear over different rings Jun 8, 2024
@mathlib-bors mathlib-bors bot closed this Jun 8, 2024
@mathlib-bors mathlib-bors bot deleted the mans0954/BilinearMap-compl branch June 8, 2024 21:54
AntoineChambert-Loir pushed a commit that referenced this pull request Jun 20, 2024
@mans0954 @AntoineChambert-Loir
refactor(LinearAlgebra/BilinearMap): Left composition, bilinear over …
71f14ab 
…different rings (#13042)

Generalise `compl₂` and `compl₁₂` for left composition with maps which are linear over different rings in the first and second variable.

Needed for #9334



Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>
@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented Jun 26, 2025

#26458 takes this generalization further.

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 approved these changes

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@mans0954 @leanprover-bot @eric-wieser