module module

`IndisputableMonolith.Physics.QuantumComputingDepthFromRS`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Physics.QuantumMolecularDesignDepthC4 module_import

declarations in this module (8)

inductive QuantumGateType L21
theorem quantumGateTypeCount L25
def pauliGroupSize L28
theorem pauliGroupSize_2cubed L29
def universalGates L32
theorem universalGates_eq_D L33
structure QuantumComputingDepthCert L35
def quantumComputingDepthCert L40