# Zulip Chat Archive

## Stream: maths

### Topic: Hermitian and semidefinite matrices

#### Yakov Pechersky (Sep 02 2020 at 20:42):

Now that we have eigenvalues, is anyone working on defining Hermitian matrices, positive semidefinite matrices, the order on them, eigendecompositions? Someone mentioned they are working on formalizing the spectral theorem.

#### Yakov Pechersky (Sep 02 2020 at 20:43):

This could use the `is_R_or_C`

class that was mentioned also.

#### Frédéric Dupuis (Sep 03 2020 at 00:13):

I'm currently working on defining inner products based on `is_R_or_C`

, so we should have complex inner products fairly soon, and hopefully stating results for both the real and complex case should be reasonable comfortable (at least I hope!). And then we can define the adjoint, Hermitian operators, and so on!

#### Frédéric Dupuis (Sep 07 2020 at 00:37):

There is now a work-in-progress PR for this here: #4057. Comments are very welcome!

#### Alexander Bentkamp (Sep 08 2020 at 14:10):

I am working on getting the theorem "generalized eigenvectors span the vectorspace" into mathlib. This should be another important ingredient of the spectral theorem, complementing @Frédéric Dupuis 's work. It will roughly look like this pull request, which I am now splitting into smaller parts: https://github.com/leanprover-community/mathlib/pull/3864

#### Frédéric Dupuis (Sep 08 2020 at 23:41):

Looks good! We'll be in very good shape soon for the spectral theorem I think.

Last updated: May 19 2021 at 02:10 UTC