mathlib

e3d36811 - feat(analysis/inner_product_space/spectrum): `pos_nonneg_eigenvalues` (#12161)

feat(analysis/inner_product_space/spectrum): `pos_nonneg_eigenvalues` (#12161) If T is a positive self-adjoint operator, then its eigenvalues are nonnegative. Maybe there should be a definition of "positive operator", and maybe this should be generalized. Guidance appreciated! Co-authored-by: Daniel Packer Co-authored-by: Hans Parshall <hparshall@users.noreply.github.com> Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>