Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

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

Open
wants to merge 10 commits into
base: master
Choose a base branch
from

Conversation

themathqueen
Copy link
Collaborator

@themathqueen themathqueen commented Apr 10, 2023

this pr shows matrix.pos_semidef iff matrix.to_euclidean_lin.is_positive (i.e., matrix semi-definite positivity corresponds to linear map positivity)


Open in Gitpod

@themathqueen themathqueen added awaiting-review The author would like community review of the PR blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. labels Apr 10, 2023
@mathlib-dependent-issues-bot
Copy link
Collaborator

This PR/issue depends on:

@eric-wieser eric-wieser added the not-too-late This PR was ready at the point mathlib3 was frozen: we will try to merge it and port it to mathlib4 label Jul 15, 2023
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
awaiting-review The author would like community review of the PR blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. not-too-late This PR was ready at the point mathlib3 was frozen: we will try to merge it and port it to mathlib4
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants