OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/FlowMatrix.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Coordinates of the actual spatial derivative in the standard orthonormal basis, preserving its determinant and identifying the divergence with trace.

  1. def OAI.ContinuumCoulomb.flowMatrix line 12
  2. def OAI.ContinuumCoulomb.flowCoordinate line 16
  3. theorem OAI.ContinuumCoulomb.flowMatrix_apply line 19
  4. theorem OAI.ContinuumCoulomb.flowMatrix_comp line 25
  5. theorem OAI.ContinuumCoulomb.flowMatrix_det line 31
  6. theorem OAI.ContinuumCoulomb.flowMatrix_trace line 35