mathlib3
feat(inner_product_space/positive): matrix.pos_semidef iff x.to_euclidean_lin.is_positive
#18786
Open
Open