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] - refactor(LinearAlgebra/SesquilinearForm): Sesquilinear Maps #9312

Closed
wants to merge 27 commits into from
Closed

[Merged by Bors] - refactor(LinearAlgebra/SesquilinearForm): Sesquilinear Maps #9312

wants to merge 27 commits into from

Conversation

mans0954
Copy link
Collaborator

@mans0954 mans0954 commented Dec 28, 2023 •
edited
Loading

Some of the concepts in LinearAlgebra/SesquilinearForm can be generalised from Sesquilinear Forms to Sesquilinear Maps with little or no impact on the rest of Mathlib. This PR makes those generalisations.

Further generalisations are likely possible, but the scope of this PR is to only consider changes which do not require non-trivial modifications to other parts of Mathlib, or other sections in SesquilinearForm.lean. Further changes can be considered in subsequent PRs if desired.

See also #9334

Open in Gitpod

@mans0954 mans0954 added the WIP Work in progress label Dec 28, 2023
@mans0954 mans0954 marked this pull request as ready for review December 28, 2023 14:16
@mans0954 mans0954 added awaiting-review and removed WIP Work in progress labels Dec 28, 2023
This was referenced Dec 30, 2023
Closed
Draft
@mans0954
Copy link
Collaborator Author

mans0954 commented Jan 6, 2024

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit ee51205.
There were no significant changes against commit b180173.

dupuisf
dupuisf reviewed Jan 14, 2024
View reviewed changes
Copy link
Contributor

@dupuisf dupuisf left a comment

Choose a reason for hiding this comment

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

I just have a few cosmetic changes, but otherwise it looks good!

Mathlib/Analysis/InnerProductSpace/Symmetric.lean Outdated Show resolved Hide resolved
Mathlib/LinearAlgebra/SesquilinearForm.lean Outdated Show resolved Hide resolved
Mathlib/LinearAlgebra/SesquilinearForm.lean Outdated Show resolved Hide resolved
@dupuisf
Copy link
Contributor

dupuisf commented Jan 14, 2024

Also, I think it might be worth changing the name of the file to SesquilinearMap.lean, but let's do it in a separate PR since renaming files makes the diffs hard to read.

@mans0954
Copy link
Collaborator Author

Also, I think it might be worth changing the name of the file to SesquilinearMap.lean, but let's do it in a separate PR since renaming files makes the diffs hard to read.

Yes, my plan was to get this PR and #9334 merged and then do a separate PR renaming both files.

j-loreaux
j-loreaux reviewed Jan 15, 2024
View reviewed changes
Copy link
Collaborator

@j-loreaux j-loreaux left a comment

Choose a reason for hiding this comment

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

I agree, looks good! Thanks! Just two minigolfs, mainly to make you aware of cool new syntax in Lean 4.

bors d+

Mathlib/LinearAlgebra/SesquilinearForm.lean Outdated Show resolved Hide resolved
Mathlib/LinearAlgebra/SesquilinearForm.lean Outdated Show resolved Hide resolved
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jan 15, 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.

@mans0954
Copy link
Collaborator Author

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Jan 16, 2024
@mans0954
refactor(LinearAlgebra/SesquilinearForm): Sesquilinear Maps (#9312)
d5ec07c 
Some of the concepts in `LinearAlgebra/SesquilinearForm` can be generalised from Sesquilinear Forms to Sesquilinear Maps with little or no impact on the rest of Mathlib. This PR makes those generalisations.

Further generalisations are likely possible, but the scope of this PR is to only consider changes which do not require non-trivial modifications to other parts of Mathlib, or other sections in `SesquilinearForm.lean`. Further changes can be considered in subsequent PRs if desired.



Co-authored-by: Christopher Hoskin <[email protected]>
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jan 16, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title refactor(LinearAlgebra/SesquilinearForm): Sesquilinear Maps [Merged by Bors] - refactor(LinearAlgebra/SesquilinearForm): Sesquilinear Maps Jan 16, 2024
@mathlib-bors mathlib-bors bot closed this Jan 16, 2024
@mathlib-bors mathlib-bors bot deleted the mans0954/SesquilinearMaps1 branch January 16, 2024 08:47
linesthatinterlace pushed a commit that referenced this pull request Jan 16, 2024
@mans0954 @linesthatinterlace
refactor(LinearAlgebra/SesquilinearForm): Sesquilinear Maps (#9312)
63d7356 
Some of the concepts in `LinearAlgebra/SesquilinearForm` can be generalised from Sesquilinear Forms to Sesquilinear Maps with little or no impact on the rest of Mathlib. This PR makes those generalisations.

Further generalisations are likely possible, but the scope of this PR is to only consider changes which do not require non-trivial modifications to other parts of Mathlib, or other sections in `SesquilinearForm.lean`. Further changes can be considered in subsequent PRs if desired.



Co-authored-by: Christopher Hoskin <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@dupuisf dupuisf dupuisf left review comments

@j-loreaux j-loreaux j-loreaux left review comments

Assignees
No one assigned
Labels
delegated
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
5 participants
@mans0954 @leanprover-bot @dupuisf @j-loreaux @leanprover-community-mathlib4-bot