mathlib3
aca9fef4 - Merge branch 'master' into inner_product_space_positive

Commit

2 years ago

Merge branch 'master' into inner_product_space_positive

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

eric-wieser

eric-wieser

Parents

Loading