Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-12 05:57 e8d0cacf

View on Github →

feat(analysis/inner_product_space/adjoint): gram lemmas (#12139) The gram operator is a self-adjoint, positive operator.

Estimated changes