mathlib3
1d048c57 - chore(analysis/inner_product_space): move definition of self-adjointness (#15281)

Commit
3 years ago
chore(analysis/inner_product_space): move definition of self-adjointness (#15281) The file `analysis/inner_product_space/basic` is way to large and since `is_self_adjoint` will be rephrased in terms of the adjoint, it should be in the `adjoint` file.
Author
Parents
Loading