mathlib3
4831680a - chore(inner_product_space/positive): some lemmas

Commit

3 years ago

chore(inner_product_space/positive): some lemmas

References

#18230 - feat(analysis/inner_product_space/positive): Positivity of linear maps

#18779 - feat(inner_product_space/positive): defines square root of a linear map

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

Author

themathqueen

themathqueen

Parents

Loading