When porting the code from https://github.com/Hayata-Yamasaki-Group/lean-quantum to Lean-QuamtumInfo,
besides moving the code to a different directory (and thus editing the imports at the tops of
files), a few changes were made:
 * Some of the `Nontrivial` and `CompleteSpace` instance variables were moved around or `omit`ted, in
   or to prevent the linter warnings about unneeded variables. This was done in:
   - BlockDiagonal.lean
   - GeneralizedPerspectiveFunction.lean
   - HilbertSchmidtOperatorSpace.lean
   - JensenOperatorInequality.lean
   - JensenOperatorInequalityIImpIV.lean
   - JensenOperatorInequalityIVtoV.lean
   - LiebAndoTrace.Lean
 * Code was moved to the "module system", adding `module`/`public import`/`@[expose]` to the start
   of each file.
 * Some whitespace was modified to make lines fit without the longLine linter complaining.

The project this code is graciously borrowed from is the work of the following:

Kazumi Kasaura (OMRON SINIC X, RIKEN)
Kei Tsukamoto (The University of Tokyo)
Kento Mori (MOLSIS)
Lisa Mizuno (The University of Tokyo)
Takahiro Namatame (Kyoto University)
Yuta Oriike (CyberAgent)
Masaya Taniguchi (RIKEN)
Sho Sonoda (RIKEN, CyberAgent)
Hayata Yamasaki (The University of Tokyo)
