OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumOrderedTripleFactors.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exact Pauli factors from the ordered three-site partition. The first two factors have matching Y parity and the last is real.

  1. def OAI.ContinuumCoulomb.QuantumOrderedTriple.first line 13
  2. def OAI.ContinuumCoulomb.QuantumOrderedTriple.second line 16
  3. def OAI.ContinuumCoulomb.QuantumOrderedTriple.third line 19
  4. def OAI.ContinuumCoulomb.QuantumOrderedTriple.pairWord line 22
  5. theorem OAI.ContinuumCoulomb.QuantumOrderedTriple.third_yCount line 25
  6. theorem OAI.ContinuumCoulomb.QuantumOrderedTriple.pair_support line 35
  7. theorem OAI.ContinuumCoulomb.QuantumOrderedTriple.pair_even line 40
  8. theorem OAI.ContinuumCoulomb.QuantumOrderedTriple.factors line 50