Skip to content
This repository was 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
themathqueen wants to merge 10 commits into
masterfrom
mon/matrix_pos
Open

feat(inner_product_space/positive): matrix.pos_semidef iff x.to_euclidean_lin.is_positive#18786
themathqueen wants to merge 10 commits into
masterfrom
mon/matrix_pos

Conversation

@themathqueen

@themathqueen themathqueen commented Apr 10, 2023

Copy link
Copy Markdown
Collaborator

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
@ghost

ghost commented Apr 10, 2023

Copy link
Copy Markdown

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.

2 participants