Expression of type ExprTuple

from the theory of proveit.physics.quantum.algebra

import proveit
# Automation is not needed when building an expression:
proveit.defaults.automation = False # This will speed things up.
proveit.defaults.inline_pngs = False # Makes files smaller.
%load_expr # Load the stored expression as 'stored_expr'
# import Expression classes needed to build the expression
from proveit import A, B, Conditional, ExprTuple, Lambda, i, n
from proveit.core_expr_types import a_1_to_n, a_i, b_1_to_n, b_i, v_1_to_n, v_i
from proveit.linear_algebra import Adj, Commutator, MatrixSpace, OrthoNormBases, ScalarMult, VecSum, VecZero
from proveit.logic import And, CartExp, Equals, Exists, Iff, InSet, Set
from proveit.numbers import Complex, Interval, one
from proveit.physics.quantum import Bra, Ket, Qmult

# build up the expression from sub-expressions
sub_expr1 = [i]
sub_expr2 = MatrixSpace(field = Complex, rows = n, columns = n)
sub_expr3 = Interval(one, n)
sub_expr4 = Qmult(Ket(v_i), Bra(v_i))
expr = ExprTuple(Lambda([A, B], Conditional(Iff(Equals(Commutator(A, B), VecZero(sub_expr2)), Exists(instance_param_or_params = [v_1_to_n], instance_expr = Exists(instance_param_or_params = [a_1_to_n, b_1_to_n], instance_expr = And(Equals(A, VecSum(index_or_indices = sub_expr1, summand = ScalarMult(a_i, sub_expr4), domain = sub_expr3)), Equals(B, VecSum(index_or_indices = sub_expr1, summand = ScalarMult(b_i, sub_expr4), domain = sub_expr3))).with_wrapping_at(2), domain = Complex).with_wrapping(), condition = InSet(Set(v_1_to_n), OrthoNormBases(CartExp(Complex, n)))).with_wrapping()).with_wrapping_at(2), And(InSet(A, sub_expr2), InSet(B, sub_expr2), Equals(Adj(A), A), Equals(Adj(B), B)))))

expr:

# check that the built expression is the same as the stored expression
assert expr == stored_expr
assert expr._style_id == stored_expr._style_id
print("Passed sanity check: expr matches stored_expr")

Passed sanity check: expr matches stored_expr

# Show the LaTeX representation of the expression for convenience if you need it.
print(stored_expr.latex())

\left(\left(A, B\right) \mapsto \left\{\begin{array}{c} \begin{array}{l} \left(\left[A, B\right] = \vec{0}\left(\mathbb{C}^{n \times n}\right)\right) \Leftrightarrow  \\ \left[\begin{array}{l}\exists_{v_{1}, v_{2}, \ldots, v_{n}~|~\left\{v_{1}, v_{2}, \ldots, v_{n}\right\} \in \textrm{O.N.Bases}\left(\mathbb{C}^{n}\right)}~\\
\left[\begin{array}{l}\exists_{a_{1}, a_{2}, \ldots, a_{n}, b_{1}, b_{2}, \ldots, b_{n} \in \mathbb{C}}~\\
\left(\begin{array}{c} \left(A = \left(\sum_{i=1}^{n} \left(a_{i} \cdot \left(\lvert v_{i} \rangle \thinspace \langle v_{i} \rvert\right)\right)\right)\right) \land  \\ \left(B = \left(\sum_{i=1}^{n} \left(b_{i} \cdot \left(\lvert v_{i} \rangle \thinspace \langle v_{i} \rvert\right)\right)\right)\right) \end{array}\right)\end{array}\right]\end{array}\right] \end{array} \end{array} \textrm{ if } A \in \mathbb{C}^{n \times n} ,  B \in \mathbb{C}^{n \times n} ,  A^{\dagger} = A ,  B^{\dagger} = B\right..\right)

stored_expr.style_options()

no style options

# display the expression information
stored_expr.expr_info()

	core type	sub-expressions	expression
0	ExprTuple	1
1	Lambda	parameters: 26 body: 2
2	Conditional	value: 3 condition: 4
3	Operation	operator: 5 operands: 6
4	Operation	operator: 59 operands: 7
5	Literal
6	ExprTuple	8, 9
7	ExprTuple	10, 11, 12, 13
8	Operation	operator: 70 operands: 14
9	Operation	operator: 38 operand: 22
10	Operation	operator: 100 operands: 16
11	Operation	operator: 100 operands: 17
12	Operation	operator: 70 operands: 18
13	Operation	operator: 70 operands: 19
14	ExprTuple	20, 21
15	ExprTuple	22
16	ExprTuple	74, 33
17	ExprTuple	76, 33
18	ExprTuple	23, 74
19	ExprTuple	24, 76
20	Operation	operator: 25 operands: 26
21	Operation	operator: 27 operand: 33
22	Lambda	parameters: 47 body: 29
23	Operation	operator: 31 operand: 74
24	Operation	operator: 31 operand: 76
25	Literal
26	ExprTuple	74, 76
27	Literal
28	ExprTuple	33
29	Conditional	value: 34 condition: 35
30	ExprTuple	74
31	Literal
32	ExprTuple	76
33	Operation	operator: 36 operands: 37
34	Operation	operator: 38 operand: 41
35	Operation	operator: 100 operands: 40
36	Literal
37	NamedExprs	field: 89 rows: 115 columns: 115
38	Literal
39	ExprTuple	41
40	ExprTuple	42, 43
41	Lambda	parameters: 44 body: 45
42	Operation	operator: 46 operands: 47
43	Operation	operator: 48 operand: 55
44	ExprTuple	50, 51
45	Conditional	value: 52 condition: 53
46	Literal
47	ExprTuple	54
48	Literal
49	ExprTuple	55
50	ExprRange	lambda_map: 56 start_index: 114 end_index: 115
51	ExprRange	lambda_map: 57 start_index: 114 end_index: 115
52	Operation	operator: 59 operands: 58
53	Operation	operator: 59 operands: 60
54	ExprRange	lambda_map: 61 start_index: 114 end_index: 115
55	Operation	operator: 62 operands: 63
56	Lambda	parameter: 96 body: 87
57	Lambda	parameter: 96 body: 88
58	ExprTuple	64, 65
59	Literal
60	ExprTuple	66, 67
61	Lambda	parameter: 96 body: 68
62	Literal
63	ExprTuple	89, 115
64	Operation	operator: 70 operands: 69
65	Operation	operator: 70 operands: 71
66	ExprRange	lambda_map: 72 start_index: 114 end_index: 115
67	ExprRange	lambda_map: 73 start_index: 114 end_index: 115
68	IndexedVar	variable: 120 index: 96
69	ExprTuple	74, 75
70	Literal
71	ExprTuple	76, 77
72	Lambda	parameter: 96 body: 78
73	Lambda	parameter: 96 body: 79
74	Variable
75	Operation	operator: 81 operand: 85
76	Variable
77	Operation	operator: 81 operand: 86
78	Operation	operator: 100 operands: 83
79	Operation	operator: 100 operands: 84
80	ExprTuple	85
81	Literal
82	ExprTuple	86
83	ExprTuple	87, 89
84	ExprTuple	88, 89
85	Lambda	parameter: 122 body: 90
86	Lambda	parameter: 122 body: 91
87	IndexedVar	variable: 106 index: 96
88	IndexedVar	variable: 107 index: 96
89	Literal
90	Conditional	value: 93 condition: 95
91	Conditional	value: 94 condition: 95
92	ExprTuple	96
93	Operation	operator: 98 operands: 97
94	Operation	operator: 98 operands: 99
95	Operation	operator: 100 operands: 101
96	Variable
97	ExprTuple	102, 104
98	Literal
99	ExprTuple	103, 104
100	Literal
101	ExprTuple	122, 105
102	IndexedVar	variable: 106 index: 122
103	IndexedVar	variable: 107 index: 122
104	Operation	operator: 108 operands: 109
105	Operation	operator: 110 operands: 111
106	Variable
107	Variable
108	Literal
109	ExprTuple	112, 113
110	Literal
111	ExprTuple	114, 115
112	Operation	operator: 116 operand: 119
113	Operation	operator: 117 operand: 119
114	Literal
115	Variable
116	Literal
117	Literal
118	ExprTuple	119
119	IndexedVar	variable: 120 index: 122
120	Variable
121	ExprTuple	122
122	Variable