mathlib

mathlib copied to clipboard

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.

---

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.

• [x] depends on: #15906

This PR/issue depends on:

• ~~leanprover-community/mathlib#15906~~ By Dependent Issues (🤖). Happy coding!

Can you merge master and fix the build? bors d+ Thanks!

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

bors merge

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests

I was using bilin_form_of_real_inner downstream; what should I be replacing it with?