[Merged by Bors] - chore(analysis/inner_product_space/basic): remove bilin_form_of_real_inner#15780
[Merged by Bors] - chore(analysis/inner_product_space/basic): remove bilin_form_of_real_inner#15780
bilin_form_of_real_inner#15780Conversation
mcdoll
added
awaiting-CI
mcdoll
added
the
awaiting-review
github-actions
bot
removed
the
awaiting-CI
| /-- The inner product as a sesquilinear form. -/ | ||
| /-- The inner product as a sesquilinear form. | ||
|
|
||
| Note that in the case `𝕜 = ℝ` this is a bilinear form. -/ |
There was a problem hiding this comment.
Can you include the recipe to obtain a bilin_form from this?
There was a problem hiding this comment.
Right now bilin_form is quite heavily linked to quadratic_form, so we can't burn all the bridges to bilin_form just yet.
There was a problem hiding this comment.
I would not be against having this PR open for a bit until I have removed the dependency of bilin_form in quadratic_form. I was looking at that as well, but I thought this one was super easy to do.
There was a problem hiding this comment.
I've added a dependence, so that it does not sit in the review queue
ghost
added
the
blocked-by-other-PR
ghost
removed
the
blocked-by-other-PR
|
This PR/issue depends on: |
|
Can you merge master and fix the build? |
|
✌️ mcdoll can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
|
bors merge |
…_inner` (#15780) Remove `bilin_form_of_real_inner` and add a remark in the docstring of `sesq_form_of_inner` that for over real spaces the sesquilinear form is by definition a bilinear form. For this we generalize `is_self_adjoint_iff_bilin_form` from `real` to `is_R_or_C` and slightly generalize `linear_map.is_self_adjoint` and `linear_map.is_adjoint_pair` to allow for conjugate linear maps in the second argument.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
bilin_form_of_real_innerbilin_form_of_real_inner
|
I was using |
…inner` I was using this downstream as `bilin_form_of_real_inner.to_quadratic_form`, and I don't see a clear replacement. Until we have api connecting sesquilinear forms with quadratic forms, we should not remove `bilin_form` API. This partially reverts #15780.
3 participants
Remove
bilin_form_of_real_innerand add a remark in the docstring ofsesq_form_of_innerthat for over real spaces the sesquilinear form is by definition a bilinear form.For this we generalize
is_self_adjoint_iff_bilin_formfromrealtois_R_or_Cand slightly generalizelinear_map.is_self_adjointandlinear_map.is_adjoint_pairto allow for conjugate linear maps in the second argument.This should be rather easy to review. Note that some of the definitions could be generalized even further, but the point was just to generalize enough to remove the
bilin_formdefinition.