OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumOrderedXZTerm.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Deterministic X/Z term classification from a list of at most two sites. The order of pair endpoints is the supplied order, with no finite-set choice.

  1. def OAI.ContinuumCoulomb.QuantumOrderedXZTerm.axis line 12
  2. theorem OAI.ContinuumCoulomb.QuantumOrderedXZTerm.axis_spec line 14
  3. def OAI.ContinuumCoulomb.QuantumOrderedXZTerm.field line 18
  4. def OAI.ContinuumCoulomb.QuantumOrderedXZTerm.ofSites line 21
  5. theorem OAI.ContinuumCoulomb.QuantumOrderedXZTerm.outside line 31
  6. theorem OAI.ContinuumCoulomb.QuantumOrderedXZTerm.field_word line 37
  7. theorem OAI.ContinuumCoulomb.QuantumOrderedXZTerm.word_eq line 43
  8. theorem OAI.ContinuumCoulomb.QuantumOrderedXZTerm.matrix_eq line 88