Proof of proveit.linear_algebra.scalar_multiplication.factorization_from_vectors theorem

import proveit
from proveit import defaults
from proveit import k
theory = proveit.Theory() # the theorem's theory
from proveit.linear_algebra.scalar_multiplication import distribution_over_vectors

%proving factorization_from_vectors

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
factorization_from_vectors:
(see dependencies)

%qed

proveit.linear_algebra.scalar_multiplication.factorization_from_vectors has been proven.

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	2, 3	, , ,  ⊢
	: , :
2	theorem		⊢
	proveit.logic.equality.equals_reversal
3	instantiation	4, 5, 6, 7, 8	, , ,  ⊢
	:
4	conjecture		⊢
	proveit.linear_algebra.scalar_multiplication.distribution_over_vectors
5	assumption		⊢
6	assumption		⊢
7	assumption		⊢
8	assumption		⊢