OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumXZFamilySplit.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

The actual word family splits into the three kinds of physical simulator terms.

  1. structure OAI.ContinuumCoulomb.QMAXZPair line 13
  2. structure OAI.ContinuumCoulomb.QMAXZField line 20
  3. def OAI.ContinuumCoulomb.QMAXZTerm.IsPair line 24
  4. def OAI.ContinuumCoulomb.QMAXZTerm.IsField line 28
  5. def OAI.ContinuumCoulomb.QMAXZTerm.IsScalar line 32
  6. def OAI.ContinuumCoulomb.QMAXZTerm.asPair line 36
  7. def OAI.ContinuumCoulomb.QMAXZTerm.asField line 42
  8. theorem OAI.ContinuumCoulomb.QMAXZTerm.pair_matrix line 48
  9. theorem OAI.ContinuumCoulomb.QMAXZTerm.field_matrix line 53
  10. theorem OAI.ContinuumCoulomb.QMAXZTerm.scalar_matrix line 57
  11. theorem OAI.ContinuumCoulomb.qmaXZLabel_ne_zero line 60
  12. theorem OAI.ContinuumCoulomb.QMAXZTerm.pair_support line 63
  13. abbrev OAI.ContinuumCoulomb.QMAXZPairIndex line 87
  14. abbrev OAI.ContinuumCoulomb.QMAXZFieldIndex line 88
  15. abbrev OAI.ContinuumCoulomb.QMAXZScalarIndex line 89
  16. def OAI.ContinuumCoulomb.qmaXZPairData line 91
  17. def OAI.ContinuumCoulomb.qmaXZFieldData line 94
  18. theorem OAI.ContinuumCoulomb.qmaXZPairData_distinct line 98
  19. theorem OAI.ContinuumCoulomb.qmaSum_subtype_ite line 113
  20. theorem OAI.ContinuumCoulomb.qmaXZFamily_split line 127
  21. def OAI.ContinuumCoulomb.qmaXZFamilyConstant line 165
  22. theorem OAI.ContinuumCoulomb.qmaXZFamily_target line 170