OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumXZSupported.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Two-local X/Z reduction with a nested, explicit mediator support.

  1. theorem OAI.ContinuumCoulomb.qmaTwoLocalXZ_supported line 14