psd matrices

Stream: Is there code for X?

[Alex Zhang]

Are positive semidefinite matrices defined in Mathlib? I only found "positive definite quadratic form" defined.

[Heather Macbeth]

Can you use the quadratic form definition in your application, or do you want something for endomorphisms?

[Eric Wieser]

Presumably you can chain docs#matrix.to_bilin with docs#bilin_form.to_quadratic_form, and then talk about M.to_bilin.to_quadratic_form.pos_def?

[Eric Wieser]

I guess that doesn't handle the S of psd

[Alex Zhang]

I think I am going to define them for matrices directly and prove lemmas connecting it to the defs for quadratic form perhaps.