OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumEightBasis.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The two encoded blocks are eight ordinary physical spins.

  1. def OAI.ContinuumCoulomb.qmaEightBasisEquiv line 13
  2. theorem OAI.ContinuumCoulomb.qmaEightTensor_source line 29
  3. theorem OAI.ContinuumCoulomb.qmaEightPauli_left line 40
  4. theorem OAI.ContinuumCoulomb.qmaEightPauli_right line 69
  5. theorem OAI.ContinuumCoulomb.qmaFourCross_source line 98