OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumForkListFullDegree.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The complete literal exchange list has degree at most three once each active group has at most three ports.

  1. abbrev OAI.ContinuumCoulomb.QuantumForkList.PortIndex line 14
  2. def OAI.ContinuumCoulomb.QuantumForkList.portSite line 16
  3. theorem OAI.ContinuumCoulomb.QuantumForkList.portSite_injective line 19
  4. def OAI.ContinuumCoulomb.QuantumForkList.asForkPorts line 26
  5. def OAI.ContinuumCoulomb.QuantumForkList.asForkState line 36
  6. theorem OAI.ContinuumCoulomb.QuantumForkList.active_index_sum line 55
  7. theorem OAI.ContinuumCoulomb.QuantumForkList.full_degree_eq line 71
  8. theorem OAI.ContinuumCoulomb.QuantumForkList.full_degree_le_three line 83