positive): Positivity of linear maps
#18230

Open

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

themathqueen wants to merge 18 commits into master from inner_product_space_positive

chore(inner_product_space/positive): some lemmas

4831680a

themathqueen added awaiting-review

themathqueen changed the title ~~chore(inner_product_space/positive): some lemmas~~ feat(inner_product_space/positive): some lemmas 2 years ago

themathqueen requested a review from

ADedecker 2 years ago

YaelDillies commented on 2023-01-22

ADedecker commented on 2023-01-22

ADedecker removed awaiting-review

ADedecker added awaiting-author

ADedecker added t-analysis

fix

4c0719b7

themathqueen added WIP

changes after review

bcafe443

fix

d0161f0f

themathqueen removed WIP

themathqueen removed awaiting-author

themathqueen added awaiting-review

themathqueen changed the title ~~feat(inner_product_space/positive): some lemmas~~ feat(inner_product_space/positive): proving results for positive linear maps over (finite-dimensional) inner product spaces 2 years ago

eric-wieser commented on 2023-02-01

YaelDillies removed awaiting-review

YaelDillies added awaiting-author

mathlib-dependent-issues-bot added blocked-by-other-PR

YaelDillies added merge-conflict

eric-wieser commented on 2023-03-31

mathlib-dependent-issues-bot removed blocked-by-other-PR

Merge branch 'master' into inner_product_space_positive

aca9fef4

delete pairwise_orthogonal

85b8249e

fixes

bce4f554

YaelDillies removed merge-conflict

YaelDillies added awaiting-CI

change name and remove lemma

e8b14bde

github-actions removed awaiting-CI

move results to new pr

ee544c3f

themathqueen changed the title ~~feat(inner_product_space/positive): proving results for positive linear maps over (finite-dimensional) inner product spaces~~ feat(inner_product_space/positive): defines positivity of linear maps 2 years ago

remove nonneg def

0500a32b

themathqueen removed awaiting-author

themathqueen added awaiting-review

YaelDillies commented on 2023-04-10

fix

8c90ed60

YaelDillies changed the title ~~feat(inner_product_space/positive): defines positivity of linear maps~~ feat(analysis/inner_product_space/positive): Positivity of linear maps 2 years ago

eric-wieser commented on 2023-04-12

update def

27965f4a

themathqueen requested a review from

eric-wieser 2 years ago

reorder lemmas

258fe88e

eric-wieser commented on 2023-04-13

add simp

384a18e8

YaelDillies commented on 2023-04-13

add protected

d7ad6ab0

remove continuous_linear_map.is_positive

a99bdf43

themathqueen added awaiting-CI

fix

f643232b

github-actions removed awaiting-CI

themathqueen requested a review from

eric-wieser 2 years ago

mcdoll commented on 2023-04-14

eric-wieser commented on 2023-04-14

remove lemmas

c81aeeeb

kim-em commented on 2023-05-02

eric-wieser added not-too-late

j-loreaux removed not-too-late

j-loreaux removed awaiting-review

j-loreaux added not-ready-to-merge

Reviewers

j-loreaux

kim-em

eric-wieser

mcdoll

YaelDillies

jsm28

ADedecker

Assignees

No one assigned

Labels

not-ready-to-merge t-analysis

Milestone

No milestone

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

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

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

Open