mathlib3
feat(inner_product_space/positive): matrix.pos_semidef iff x.to_euclidean_lin.is_positive
#18786
Open
Overview
Commits
10
Changes
View On GitHub

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

themathqueen wants to merge 10 commits into master from mon/matrix_pos
themathqueen
themathqueen chore(inner_product_space/positive): some lemmas
4831680a
themathqueen fix
4c0719b7
themathqueen changes after review
bcafe443
themathqueen fix
d0161f0f
eric-wieser Merge branch 'master' into inner_product_space_positive
aca9fef4
eric-wieser delete pairwise_orthogonal
85b8249e
themathqueen fixes
bce4f554
themathqueen change name and remove lemma
e8b14bde
themathqueen move results to new pr
ee544c3f
themathqueen feat(inner_product_space/positive): matrix.pos_semidef iff x.to_eucli…
8b9324da
themathqueen themathqueen added awaiting-review
themathqueen themathqueen added blocked-by-other-PR
mathlib-dependent-issues-bot
eric-wieser eric-wieser added not-too-late

Login to write a write a comment.

Login via GitHub

Reviewers
No reviews
Assignees
No one assigned
Labels
awaiting-review blocked-by-other-PR not-too-late
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum