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.
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
[Merged by Bors] - chore(analysis/inner_product_space/basic): remove bilin_form_of_real_inner
#15780
Conversation
/-- 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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can you include the recipe to obtain a bilin_form
from this?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I've added a dependence, so that it does not sit in the review queue
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 |
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: |
bilin_form_of_real_inner
bilin_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.
Remove
bilin_form_of_real_inner
and add a remark in the docstring ofsesq_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
fromreal
tois_R_or_C
and slightly generalizelinear_map.is_self_adjoint
andlinear_map.is_adjoint_pair
to 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_form
definition.