mathlib3

e8d0cacf - feat(analysis/inner_product_space/adjoint): gram lemmas (#12139)

feat(analysis/inner_product_space/adjoint): gram lemmas (#12139) The gram operator is a self-adjoint, positive operator. Co-authored-by: Hans Parshall <hparshall@users.noreply.github.com>