OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumTensorPairLinear.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Bilinearity of two-site placements in the finite tensor product.

  1. theorem OAI.ContinuumCoulomb.qmaSiteMatrix_sum line 14
  2. theorem OAI.ContinuumCoulomb.qmaPairMatrix_sum_left line 19
  3. theorem OAI.ContinuumCoulomb.qmaPairMatrix_sum_right line 24
  4. theorem OAI.ContinuumCoulomb.qmaPairMatrix_one_right line 30
  5. theorem OAI.ContinuumCoulomb.qmaPairMatrix_one_left line 35