mathlib3

8b981918 - feat(analysis/inner_product_space): the adjoint for unbounded operators (#18820)