# Zulip Chat Archive

## Stream: general

### Topic: Inner product spaces

#### Alexander Bentkamp (Mar 15 2019 at 20:15):

Hello,

Is there anyone else currently interested in inner product spaces? I'd like to start working on this.

I found this formalization:

https://github.com/ImperialCollegeLondon/xena-UROP-2018/blob/master/src/inner_product_spaces/basic.lean.

@Andreas Swerdlow Are there still plans to bring this into mathlib?

I am also aware of the Lean2 formalization: https://github.com/leanprover/lean2/blob/master/library/theories/analysis/inner_product.lean

The ImperialCollege formalization is over complex numbers and the Lean2 formalization is over the reals. I am interested in the reals, but I will try to find a generalization that subsumes both. Are there any concepts like this already?

#### Johan Commelin (Mar 15 2019 at 20:19):

There is the whole theory of quadratic forms, which works over any field (though characteristic 2 can be hairy).

#### Johan Commelin (Mar 15 2019 at 20:20):

Then you can specialise to nondegenerate forms, symmetric forms, alternating forms, hermitian forms, etc...

#### Kevin Buzzard (Mar 15 2019 at 20:30):

In number theory we define unitary groups in the setting where K is a field (say) and L/K is a finite etale K-algebra of degree 2, which is a fancy way of saying either L=K+K or L is a separable quadratic extension of K. The non-trivial K-automorphism of L is denoted c, say (c for complex conjugation if K=real and L=complex) and then one can consider a non-degenerate hermitian sesquilinear form on an L-vector space. For it to be positive definite you need some notion of positive though, so then K should embed into the reals.

#### Alexander Bentkamp (Mar 15 2019 at 20:54):

Ok, thanks. I'll see what I can do.

#### Andreas Swerdlow (Mar 16 2019 at 02:41):

I was thinking of submitting to mathlib fairly soon. A more up to date version is available here: https://github.com/leanprover-fork/mathlib-backup/blob/inner_product_spaces/linear_algebra/herm_inner_product_space.lean

#### Alexander Bentkamp (Mar 16 2019 at 17:34):

I have transferred the Lean2 formalization to Lean3 now. It's for real vector spaces only. Let's see if we can merge after you submit to mathlib.

Last updated: May 14 2021 at 05:20 UTC