Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-13 12:42 1d048c57

View on Github →

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.

Estimated changes