Hilbert spaces

Stream: new members

[Horatiu Cheval]

A very basic mathlib question, just to be sure. As far as I can tell, there is no Hilbert space class in mathlib. Then, what would be the recommended way of saying "Let $H$ be a real Hilbert space"? Would

variables {H : Type*} [inner_product_space ℝ H] [complete_space H]

be the way to go?

[Horatiu Cheval]

And also the analogous question for Banach spaces.

[Rémy Degenne]

Yes, that would be the way to do it. For Banach spaces, replace inner_product_space with normed_space. You may need [normed_group H] to be able to have [normed_space R H].