Global Index

A

adjoint [definition, in Matrix]
adjoint_compat [lemma, in Matrix]
adjoint_involutive [lemma, in Matrix]
app [constructor, in SQIMP]

B

bell [definition, in Multiqubit]
bell_com [definition, in SQIMP]
bound [definition, in Real]
bound_sqrt2 [lemma, in Real]
BtoN [definition, in SQIMP]

C

C [definition, in Complex]
Cconj [definition, in Complex]
Cconj_involutive [lemma, in Complex]
Cconj_mult_distr [lemma, in Complex]
Cconj_opp [lemma, in Complex]
Cconj_plus_distr [lemma, in Complex]
Cconj_R [lemma, in Complex]
Cconj_rad2 [lemma, in Complex]
Cconj_0 [lemma, in Complex]
Cdiv [definition, in Complex]
Ci [definition, in Complex]
Cinv [definition, in Complex]
Cinv_l [lemma, in Complex]
Cinv_r [lemma, in Complex]
Cminus [definition, in Complex]
Cmult [definition, in Complex]
Cmult_assoc [lemma, in Complex]
Cmult_comm [lemma, in Complex]
Cmult_plus_distr_l [lemma, in Complex]
Cmult_plus_distr_r [lemma, in Complex]
Cmult_0_l [lemma, in Complex]
Cmult_0_r [lemma, in Complex]
Cmult_1_l [lemma, in Complex]
Cmult_1_r [lemma, in Complex]
Cnorm [definition, in Complex]
Cnorm2 [definition, in Complex]
CNOT [definition, in Multiqubit]
CNOTp1 [lemma, in Multiqubit]
CNOT' [definition, in SQIMP]
CNOT00 [lemma, in Multiqubit]
CNOT01 [lemma, in Multiqubit]
CNOT10 [lemma, in Multiqubit]
CNOT11 [lemma, in Multiqubit]
com [inductive, in SQIMP]
completeness [axiom, in Real]
Complex [library]
com_equiv [definition, in SQIMP]
com_equiv_refl [lemma, in SQIMP]
com_equiv_sym [lemma, in SQIMP]
com_equiv_trans [lemma, in SQIMP]
Conj_mult_norm2 [lemma, in Complex]
Copp [definition, in Complex]
Copp_involutive [lemma, in Complex]
Copp_mult_distr_l [lemma, in Complex]
Copp_mult_distr_r [lemma, in Complex]
Cplus [definition, in Complex]
Cplus_assoc [lemma, in Complex]
Cplus_comm [lemma, in Complex]
Cplus_opp_l [lemma, in Complex]
Cplus_opp_r [lemma, in Complex]
Cplus_0_l [lemma, in Complex]
Cplus_0_r [lemma, in Complex]
Csqrt2_inv [lemma, in Qubit]
Csqrt2_square [lemma, in Complex]
Csqrt_inv [lemma, in Qubit]
Csum [definition, in Complex]
Csum_conj_distr [lemma, in Complex]
Csum_eq [lemma, in Complex]
Csum_mult_l [lemma, in Complex]
Csum_mult_r [lemma, in Complex]
Csum_plus [lemma, in Complex]
Csum_unique [lemma, in Complex]
Csum_0 [lemma, in Complex]
C₀ [definition, in Complex]
C₁ [definition, in Complex]
C1_neq_C₀ [lemma, in Complex]
C_Field_Theory [lemma, in Complex]
c_proj_eq [lemma, in Complex]

D

decode [definition, in SQIMP]
dot [definition, in Matrix]

E

encode [definition, in SQIMP]
eval [definition, in SQIMP]
eval_bell [lemma, in SQIMP]
eval_cnot [definition, in SQIMP]
ex_lt_sqrt2 [lemma, in Real]

F

field_test1 [definition, in Real]

G

Gate [inductive, in SQIMP]
G_CNOT [constructor, in SQIMP]
g_eval [definition, in SQIMP]
G_H [constructor, in SQIMP]
G_X [constructor, in SQIMP]
G_Z [constructor, in SQIMP]

H

H [definition, in Qubit]
HH₀₁ [lemma, in Multiqubit]
Hplus [lemma, in Qubit]
Htwice [lemma, in Qubit]
H' [definition, in SQIMP]

I

I [definition, in Matrix]
inner_product [definition, in Matrix]
INR [definition, in Real]
is_lub [definition, in Real]
is_upper_bound [definition, in Real]

K

kron [definition, in Matrix]
kron_adjoint [lemma, in Matrix]
kron_compat [lemma, in Matrix]

L

lt_sqrt2 [definition, in Real]

M

N

NOTC [definition, in SQIMP]

O

outer_product [definition, in Matrix]

P

pad [definition, in SQIMP]
partial_measure_bell [lemma, in Multiqubit]
partial_measure_plus_minus [lemma, in Multiqubit]
pown_sqrt [lemma, in Qubit]
pow2_sqrt [lemma, in Qubit]
pow2_sqrt2 [lemma, in Qubit]

Q

qubit [definition, in Multiqubit]
Qubit [abbreviation, in Qubit]
Qubit [library]
Qubits [abbreviation, in Multiqubit]
qubit0 [definition, in Qubit]
qubit1 [definition, in Qubit]
qubit_decomposition [lemma, in Qubit]
q_minus [definition, in Qubit]
q_plus [definition, in Qubit]