mathlib
a99bdf43 - remove continuous_linear_map.is_positive

Commit

3 years ago

remove continuous_linear_map.is_positive

References

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

Author

themathqueen

themathqueen

Parents

Loading