OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumOrderedTriple.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A deterministic three-site partition for the third-order gadget. For three sites the last factor is the first available non-Y letter; shorter lists give an empty last factor.

  1. def OAI.ContinuumCoulomb.QuantumOrderedTriple.partition line 15
  2. theorem OAI.ContinuumCoulomb.QuantumOrderedTriple.partition_spec line 22
  3. theorem OAI.ContinuumCoulomb.QuantumOrderedTriple.partition_nodup line 46
  4. theorem OAI.ContinuumCoulomb.QuantumOrderedTriple.pair_nodup line 50
  5. theorem OAI.ContinuumCoulomb.QuantumOrderedTriple.partition_cover line 57
  6. theorem OAI.ContinuumCoulomb.QuantumOrderedTriple.partition_disjoint line 65
  7. theorem OAI.ContinuumCoulomb.QuantumOrderedTriple.not_three_y line 71
  8. theorem OAI.ContinuumCoulomb.QuantumOrderedTriple.real_part line 90