mathlib3
feat(inner_product_space/positive): defines square root of a linear map
#18779

Open

feat(inner_product_space/positive): defines square root of a linear map #18779

themathqueen wants to merge 10 commits into master from mon/ips_positive

chore(inner_product_space/positive): some lemmas

4831680a

fix

4c0719b7

changes after review

bcafe443

fix

d0161f0f

Merge branch 'master' into inner_product_space_positive

aca9fef4

delete pairwise_orthogonal

85b8249e

fixes

bce4f554

change name and remove lemma

e8b14bde

move results to new pr

ee544c3f

feat(inner_product_space/positive): define linear_map.sqrt

a8551bbd

themathqueen added blocked-by-other-PR

themathqueen added t-analysis

themathqueen added awaiting-review

eric-wieser added not-too-late

j-loreaux removed awaiting-review

j-loreaux removed not-too-late

j-loreaux added not-ready-to-merge

Reviewers

No reviews

Assignees

No one assigned

Labels

blocked-by-other-PR not-ready-to-merge t-analysis

Milestone

No milestone