OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumOrderedLabelYY.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exact sparse letters for YY removal and the final private-pair split. Zero-labelled entries are retained so support-list order stays literal.

  1. def OAI.ContinuumCoulomb.QuantumOrderedLabelData.zeros line 15
  2. def OAI.ContinuumCoulomb.QuantumOrderedLabelData.yyFactors line 17
  3. def OAI.ContinuumCoulomb.QuantumOrderedLabelData.yyBlock line 23
  4. def OAI.ContinuumCoulomb.QuantumOrderedLabelData.privateBlock line 27
  5. theorem OAI.ContinuumCoulomb.QuantumOrderedLabelData.tag_zeros line 31
  6. theorem OAI.ContinuumCoulomb.QuantumOrderedLabelData.yyFactors_tag line 36
  7. theorem OAI.ContinuumCoulomb.QuantumOrderedLabelData.yyBlock_tag line 66
  8. theorem OAI.ContinuumCoulomb.QuantumOrderedLabelData.privateBlock_tag line 92