The "quantum" algebra is defined by algebra on Hilbert spaces, inner product spaces over complex numbers. Bra and ket notation is defined in this package, as well as Qmult for "multiplying" a sequence of bra's, ket's, and/or quantum operators.

In [1]:

importproveit%theory # toggles between interactive and static modes