[Merged by Bors] - refactor(LinearAlgebra/SesquilinearForm): Sesquilinear Maps#9312
[Merged by Bors] - refactor(LinearAlgebra/SesquilinearForm): Sesquilinear Maps#9312
Conversation
|
!bench |
|
Here are the benchmark results for commit ee51205. |
dupuisf
left a comment
There was a problem hiding this comment.
I just have a few cosmetic changes, but otherwise it looks good!
|
Also, I think it might be worth changing the name of the file to |
Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>
Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>
Yes, my plan was to get this PR and #9334 merged and then do a separate PR renaming both files. |
j-loreaux
left a comment
There was a problem hiding this comment.
I agree, looks good! Thanks! Just two minigolfs, mainly to make you aware of cool new syntax in Lean 4.
bors d+
|
✌️ mans0954 can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
|
bors r+ |
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 <mans0954@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded: |
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 <mans0954@users.noreply.github.com>
Some of the concepts in
LinearAlgebra/SesquilinearFormcan 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