environ
vocabularies HIDDEN, NUMBERS, NAT_1, VECTSP_1, SUBSET_1, MATRIX_1, FINSEQ_2, ZFMISC_1, RELAT_1, TARSKI, CARD_1, ARYTM_3, FUNCT_1, FREEALG, FINSET_1, FINSEQ_1, MESFUNC1, GROUP_1, SUPINF_2, LAPLACE, XBOOLE_0, ARYTM_1, XXREAL_0, POLYNOM1, POLYNOM2, MATRIX_3, CARD_3, AFINSQ_1, ORDINAL4, POLYNOM3, STRUCT_0, PARTFUN1, RANKNULL, RLSUB_1, RLVECT_5, PRVECT_1, RLVECT_3, ALGSTR_0, VECTSP10, MATRLIN, MATRLIN2, POLYNOM5, NEWTON, MONOID_0, BINOP_1, RLVECT_1, LATTICES, RLSUB_2, FINSEQ_4, MCART_1, RLVECT_2, VALUED_1, FUNCT_2, VECTSP11, MSSUBFAM, UNIALG_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, CARD_1, XCMPLX_0, ALGSTR_0, XXREAL_0, FINSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, NAT_1, FINSEQ_1, BINOP_1, STRUCT_0, RLVECT_1, GROUP_1, VECTSP_1, FINSEQ_2, MATRIX_0, MATRIX_1, NAT_D, GROUP_4, MATRIX_3, DOMAIN_1, MEASURE6, PRVECT_1, VECTSP_4, VECTSP_5, VECTSP_6, VECTSP_7, VECTSP_9, FINSEQOP, MATRIX13, MATRLIN, LAPLACE, MOD_2, RANKNULL, POLYNOM3, MONOID_0, ALGSEQ_1, POLYNOM4, POLYNOM5, MATRLIN2;
definitions TARSKI, XBOOLE_0;
theorems ZFMISC_1, RLVECT_1, MATRIX_0, MATRIX_3, VECTSP_1, NAT_1, FINSEQ_1, FINSEQ_3, FINSEQ_2, CARD_1, CARD_2, FINSEQOP, FINSOP_1, FUNCT_1, FUNCT_2, FVSUM_1, GROUP_1, LAPLACE, MATRIX13, MATRIXR2, MATRLIN, ORDINAL1, PARTFUN1, RELAT_1, STIRL2_1, STRUCT_0, TARSKI, VECTSP_4, VECTSP_5, VECTSP_6, VECTSP_7, VECTSP_9, VECTSP10, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, MOD_2, RANKNULL, MONOID_0, GROUP_4, SYSREL, SUBSET_1, FINSEQ_5, ALGSEQ_1, POLYNOM4, POLYNOM5, HILBASIS, MATRIXJ1, MATRLIN2, VALUED_0, NAT_D, RLVECT_2, MATRIX_1;
schemes NAT_1, FUNCT_2;
registrations XBOOLE_0, FUNCT_1, FINSET_1, STRUCT_0, VECTSP_1, FUNCT_2, ORDINAL1, XXREAL_0, NAT_1, FINSEQ_1, FINSEQ_2, SEQM_3, MATRIX13, XREAL_0, VECTSP_9, RANKNULL, POLYNOM3, POLYNOM5, MONOID_0, CARD_1, RELSET_1, MOD_2, GRCAT_1, PRVECT_1, MATRLIN2;
constructors HIDDEN, FINSOP_1, GROUP_4, VECTSP_7, VECTSP_9, MATRIX13, REALSET1, LAPLACE, VECTSP_5, RANKNULL, MONOID_0, POLYNOM4, POLYNOM5, MATRLIN2, BINOP_2, RELSET_1, MATRIX_1, ALGSEQ_1;
requirements HIDDEN, ARITHM, NUMERALS, REAL, BOOLE, SUBSET;
equalities STRUCT_0, RLVECT_1, FINSEQ_1, VECTSP_4, FVSUM_1, LAPLACE, MATRIX13, RANKNULL, VECTSP_6, MATRLIN2;
expansions STRUCT_0, TARSKI, XBOOLE_0, VECTSP_4;
theorem Th4:
for
i,
j,
n being
Nat for
K being
Field for
A,
B being
Matrix of
n,
K st
i in Seg n &
j in Seg n holds
Delete (
(A + B),
i,
j)
= (Delete (A,i,j)) + (Delete (B,i,j))
Lm1:
for K being Field
for V1, V2 being VectSp of K
for f being linear-transformation of V1,V2
for W1 being Subspace of V1
for W2 being Subspace of V2
for F being Function of W1,W2 st F = f | W1 holds
F is linear-transformation of W1,W2
Lm2:
for K being Field
for V being non trivial VectSp of K holds
( id V is with_eigenvalues & ex v being Vector of V st
( v <> 0. V & (id V) . v = (1_ K) * v ) )
Lm3:
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for a, b being Scalar of K holds (a * b) * f = a * (b * f)
Lm4:
for K being Field
for V1 being VectSp of K
for L being Scalar of K
for f, g being Function of V1,V1 holds L * (f * g) = (L * f) * g
Lm5:
for K being Field
for V1 being VectSp of K
for L being Scalar of K
for f, g being Function of V1,V1 st f is additive & f is homogeneous holds
L * (f * g) = f * (L * g)
Lm6:
for K being Field
for V1 being VectSp of K
for f1, f2, g being Function of V1,V1 holds (f1 + f2) * g = (f1 * g) + (f2 * g)
Lm7:
for K being Field
for V1 being VectSp of K
for f1, f2, g being Function of V1,V1 st g is additive & g is homogeneous holds
g * (f1 + f2) = (g * f1) + (g * f2)
Lm8:
for K being Field
for V1 being VectSp of K
for f1, f2, f3 being Function of V1,V1 holds (f1 + f2) + f3 = f1 + (f2 + f3)
Lm9:
for n being Nat
for K being Field
for V1 being VectSp of K
for L being Scalar of K holds (L * (id V1)) |^ n = ((power K) . (L,n)) * (id V1)
Lm10:
for K being Field
for V1 being VectSp of K
for f being linear-transformation of V1,V1
for a, b being Scalar of K holds (a + b) * f = (a * f) + (b * f)