Theorem tensor_prod_of_linear_maps of type Forall ¶

from the theory of proveit.linear_algebra.tensors ¶

In [1]:

import proveit
# Automation is not needed when only building an expression:
proveit.defaults.automation = False # This will speed things up.
proveit.defaults.inline_pngs = False # Makes files smaller.
%load_theorem_expr # Load the stored theorem expression as 'stored_expr'
# import the special expression
from proveit.linear_algebra.tensors import tensor_prod_of_linear_maps

In [2]:

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

Passed sanity check: tensor_prod_of_linear_maps matches stored_expr

In [3]:

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

\forall_{K}~\left[\forall_{n \in \mathbb{N}^+}~\left[\begin{array}{l}\forall_{V_{1}, V_{2}, \ldots, V_{n}, W_{1}, W_{2}, \ldots, W_{n} \underset{{\scriptscriptstyle c}}{\in} \textrm{VecSpaces}\left(K\right)}~\\
\left[\begin{array}{l}\forall_{\left(A_{1} \in \mathcal{L}\left(V_{1}, W_{1}\right)\right), \left(A_{2} \in \mathcal{L}\left(V_{2}, W_{2}\right)\right), \ldots, \left(A_{n} \in \mathcal{L}\left(V_{n}, W_{n}\right)\right)}~\\
\left[\begin{array}{l}\forall_{\left(v_{1} \in V_{1}\right), \left(v_{2} \in V_{2}\right), \ldots, \left(v_{n} \in V_{n}\right)}~\\
\left(\left(A_{1} {\otimes}  A_{2} {\otimes}  \ldots {\otimes}  A_{n}\right)\left(v_{1} {\otimes}  v_{2} {\otimes}  \ldots {\otimes}  v_{n}\right) = \left(A_{1}\left(v_{1}\right) {\otimes}  A_{2}\left(v_{2}\right) {\otimes}  \ldots {\otimes}  A_{n}\left(v_{n}\right)\right)\right)\end{array}\right]\end{array}\right]\end{array}\right]\right]

In [4]:

stored_expr.style_options()

name	description	default	current value	related methods
with_wrapping	If 'True', wrap the Expression after the parameters	None	None/False	('with_wrapping',)
condition_wrapping	Wrap 'before' or 'after' the condition (or None).	None	None/False	('with_wrap_after_condition', 'with_wrap_before_condition')
wrap_params	If 'True', wraps every two parameters AND wraps the Expression after the parameters	None	None/False	('with_params',)
justification	justify to the 'left', 'center', or 'right' in the array cells	center	center	('with_justification',)

In [5]:

# display the expression information
stored_expr.expr_info()

	core type	sub-expressions
0	Operation	operator: 34 operand: 2
1	ExprTuple	2
2	Lambda	parameter: 50 body: 3
3	Operation	operator: 34 operand: 5
4	ExprTuple	5
5	Lambda	parameter: 84 body: 7
6	ExprTuple	84
7	Conditional	value: 8 condition: 9
8	Operation	operator: 34 operand: 12
9	Operation	operator: 75 operands: 11
10	ExprTuple	12
11	ExprTuple	84, 13
12	Lambda	parameters: 14 body: 15
13	Literal
14	ExprTuple	16, 17
15	Conditional	value: 18 condition: 19
16	ExprRange	lambda_map: 20 start_index: 83 end_index: 84
17	ExprRange	lambda_map: 21 start_index: 83 end_index: 84
18	Operation	operator: 34 operand: 24
19	Operation	operator: 53 operands: 23
20	Lambda	parameter: 92 body: 81
21	Lambda	parameter: 92 body: 70
22	ExprTuple	24
23	ExprTuple	25, 26
24	Lambda	parameters: 66 body: 27
25	ExprRange	lambda_map: 28 start_index: 83 end_index: 84
26	ExprRange	lambda_map: 29 start_index: 83 end_index: 84
27	Conditional	value: 30 condition: 31
28	Lambda	parameter: 92 body: 32
29	Lambda	parameter: 92 body: 33
30	Operation	operator: 34 operand: 40
31	Operation	operator: 53 operands: 36
32	Operation	operator: 38 operands: 37
33	Operation	operator: 38 operands: 39
34	Literal
35	ExprTuple	40
36	ExprTuple	41
37	ExprTuple	81, 42
38	Literal
39	ExprTuple	70, 42
40	Lambda	parameters: 73 body: 43
41	ExprRange	lambda_map: 44 start_index: 83 end_index: 84
42	Operation	operator: 45 operand: 50
43	Conditional	value: 47 condition: 48
44	Lambda	parameter: 92 body: 49
45	Literal
46	ExprTuple	50
47	Operation	operator: 51 operands: 52
48	Operation	operator: 53 operands: 54
49	Operation	operator: 75 operands: 55
50	Variable
51	Literal
52	ExprTuple	56, 57
53	Literal
54	ExprTuple	58
55	ExprTuple	85, 59
56	Operation	operator: 60 operand: 67
57	Operation	operator: 72 operands: 62
58	ExprRange	lambda_map: 63 start_index: 83 end_index: 84
59	Operation	operator: 64 operands: 65
60	Operation	operator: 72 operands: 66
61	ExprTuple	67
62	ExprTuple	68
63	Lambda	parameter: 92 body: 69
64	Literal
65	ExprTuple	81, 70
66	ExprTuple	71
67	Operation	operator: 72 operands: 73
68	ExprRange	lambda_map: 74 start_index: 83 end_index: 84
69	Operation	operator: 75 operands: 76
70	IndexedVar	variable: 77 index: 92
71	ExprRange	lambda_map: 78 start_index: 83 end_index: 84
72	Literal
73	ExprTuple	79
74	Lambda	parameter: 92 body: 80
75	Literal
76	ExprTuple	89, 81
77	Variable
78	Lambda	parameter: 92 body: 85
79	ExprRange	lambda_map: 82 start_index: 83 end_index: 84
80	Operation	operator: 85 operand: 89
81	IndexedVar	variable: 87 index: 92
82	Lambda	parameter: 92 body: 89
83	Literal
84	Variable
85	IndexedVar	variable: 88 index: 92
86	ExprTuple	89
87	Variable
88	Variable
89	IndexedVar	variable: 90 index: 92
90	Variable
91	ExprTuple	92
92	Variable