My quantum computation instructor keeps referring to the vector space in which he is using Dirac's bra-ket notation as an "inner product space", but doesn't it need additional properties to use that notation? In particular don't we need to
specify an implementation of the inner product in terms of some other vector space for the first argument; and
require that the inner product be linear in that argument.
The first requirement seems to be necessary to get bras in the first place (I gather there are some theorems that guarantee we can use the inner product to do this) and the second seems necessary to allow us to identify the notation with something like "multiplication" of a bra and a ket.
Does bra-ket notation work for all inner product spaces, or are additional properties required? If so, do these properties have names; does the space that has them?
Forgive the naive formulation. I may not have the language quite right.