Documentation

LeanPool.SingleCopyStabilizer.HadamardCoefficient

The normalization coefficient for arbitrary-qubit Hadamard actions.

source
noncomputable def LeanPool.SingleCopyStabilizer.QubitGates.hadamardCoefficient :
ℂ

The positive real coefficient 1 / √2, regarded as a complex number.

Equations
Instances For
    source
    theorem LeanPool.SingleCopyStabilizer.QubitGates.hadamardCoefficient_mul :
    hadamardCoefficient * hadamardCoefficient = 1 / 2
    source
    @[simp]
    theorem LeanPool.SingleCopyStabilizer.QubitGates.hadamardCoefficient_star :
    star hadamardCoefficient = hadamardCoefficient