OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumPauliReal.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Hermitian local matrices have real Pauli coefficients.

  1. theorem OAI.ContinuumCoulomb.qmaPauliCoefficient_star line 14
  2. theorem OAI.ContinuumCoulomb.qmaPauliCoefficient_real line 30
  3. theorem OAI.ContinuumCoulomb.qmaPauli_real_expansion line 36