Unitary representation

Stream: maths

[Nicolò Cavalleri]

I would like to prove that unitary representations are semisimple and thus I wonder what should be the definition of unitary representation in Lean, since I cannot find it (please point it out to me in case it already exists). Should it be just a property on general representations? Or should it be defined analogously to general representations as a morphism of $G$ into isometries of a normed vector space? I would probably implement it in the first way but I might not be seeing some problems that might appear later

[Winston Yin]

Firstly perhaps docs#representation and its related theory helps. That theory is developed quite generally, so you'll have to specialise it to Hilbert spaces, for which maybe this file is relevant: analysis.inner_product_space.adjoint