OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumGates.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Unitarity of the actual finite H,T,CNOT verifier circuits.

  1. theorem OAI.ContinuumCoulomb.qmaHadamard_gram line 13

    Distinct definitions of this name: OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumGateUnitary.lean:13 (same statement text; different proof or body). Qualify references as OAI.ContinuumCoulomb.qmaHadamard_gram@path.

  2. theorem OAI.ContinuumCoulomb.qmaPhaseT_gram line 22

    Distinct definitions of this name: OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumGateUnitary.lean:21 (same statement text; different proof or body). Qualify references as OAI.ContinuumCoulomb.qmaPhaseT_gram@path.

  3. theorem OAI.ContinuumCoulomb.qmaLocal_gram line 40
  4. theorem OAI.ContinuumCoulomb.qmaControlledNot_involutive line 51

    Distinct definitions of this name: OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumGateUnitary.lean:42 (different declaration text). Qualify references as OAI.ContinuumCoulomb.qmaControlledNot_involutive@path.

  5. theorem OAI.ContinuumCoulomb.qmaPermutation_gram line 67
  6. theorem OAI.ContinuumCoulomb.qmaQubit_val line 77
  7. theorem OAI.ContinuumCoulomb.qmaGateMatrix_gram line 80

    Distinct definitions of this name: OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumGateUnitary.lean:57 (different declaration text). Qualify references as OAI.ContinuumCoulomb.qmaGateMatrix_gram@path.

  8. theorem OAI.ContinuumCoulomb.qmaCircuitMatrix_gram line 93

    Distinct definitions of this name: OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumGateUnitary.lean:88 (same statement text; different proof or body). Qualify references as OAI.ContinuumCoulomb.qmaCircuitMatrix_gram@path.

  9. theorem OAI.ContinuumCoulomb.qmaCircuit_preserves_norm line 112