environ
vocabularies HIDDEN, NUMBERS, INT_1, XXREAL_0, CARD_1, ARYTM_1, ARYTM_3, SUBSET_1, VECTSP_1, VECTSP_2, STRUCT_0, XBOOLE_0, ALGSTR_0, SUPINF_2, NEWTON, RELAT_1, GROUP_1, BINOP_1, RLVECT_1, MESFUNC1, LATTICES, ALGSTR_1, FINSEQ_1, PARTFUN1, CARD_3, NAT_1, FUNCT_1, ORDINAL4, FINSEQ_2, TARSKI, MATRIX_1, TREES_1, INCSP_1, FVSUM_1, RVSUM_1, ZFMISC_1, ALGSEQ_1, POLYNOM1, COMPLEX1, MCART_1, POLYNOM2, POLYNOM3, POLYNOM8;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, VECTSP_2, BINOP_1, BINOM, ALGSTR_1, PARTFUN1, FINSEQ_1, FINSEQ_2, INT_1, NAT_1, NAT_D, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1, FVSUM_1, ALGSEQ_1, LOPBAN_3, POLYNOM5, POLYNOM3, MATRIX_0, MATRIX_1, MATRIX_3, POLYNOM4, XTUPLE_0, MCART_1, INT_2;
definitions ;
theorems FVSUM_1, GROUP_1, BINOM, VECTSP_1, ALGSEQ_1, NAT_1, FINSEQ_4, INT_1, FUNCT_2, XREAL_1, VECTSP_2, ALGSTR_1, MATRIX_0, FUNCT_1, MATRIX_3, FINSEQ_1, ZFMISC_1, COMPLEX1, RLVECT_1, POLYNOM4, TARSKI, MCART_1, FINSEQ_2, POLYNOM1, ABSVALUE, POLYNOM3, POLYNOM5, FINSEQ_3, ORDINAL1, XXREAL_0, FUNCOP_1, PARTFUN1, XREAL_0, XTUPLE_0, MATRIX_1, LOPBAN_3;
schemes NAT_1, FUNCT_2, MATRIX_0, FINSEQ_1, INT_1;
registrations XBOOLE_0, ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, STRUCT_0, VECTSP_1, ALGSTR_1, GCD_1, POLYNOM3, CARD_1, XTUPLE_0;
constructors HIDDEN, REAL_1, NAT_D, VECTSP_2, ALGSTR_2, TOPREAL1, MATRIX_3, POLYNOM4, POLYNOM5, BINOM, RELSET_1, FVSUM_1, XTUPLE_0, MATRIX_1, ALGSEQ_1, BINOP_1, LOPBAN_3;
requirements HIDDEN, NUMERALS, SUBSET, REAL, BOOLE, ARITHM;
equalities VECTSP_1, RLVECT_1, BINOM, FINSEQ_1, MATRIX_0, POLYNOM3, ALGSTR_0;
expansions VECTSP_1;
Lm1:
for j being Integer holds
( j >= 0 or j = - 1 or j < - 1 )
Lm2:
for j being Integer holds
( j >= 1 or j = 0 or j < 0 )
Lm3:
for L being non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr
for a being Element of L
for i being Integer st 0 > i holds
pow (a,i) = (pow (a,|.i.|)) "
Lm4:
for L being non empty non degenerated almost_left_invertible well-unital distributive associative commutative doubleLoopStr
for i being Integer
for x being Element of L st i <= 0 holds
pow (x,i) = (pow (x,|.i.|)) "
Lm5:
for L being non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr
for i being Element of NAT holds pow ((1. L),i) = 1. L
Lm6:
for L being non empty well-unital doubleLoopStr
for n being Element of NAT holds (1. L) |^ n = 1. L
Lm7:
for L being non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr
for m being Element of NAT
for x being Element of L st x <> 0. L holds
(x |^ m) * ((x ") |^ m) = 1. L
Lm8:
for L being non empty non degenerated right_complementable almost_left_invertible left-distributive well-unital add-associative right_zeroed associative commutative doubleLoopStr
for k being Element of NAT
for x being Element of L st x <> 0. L holds
(x ") |^ k = (x |^ k) "
Lm9:
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for x being Element of L st x <> 0. L holds
for n being Element of NAT holds pow ((x "),n) = (pow (x,n)) "
Lm10:
for L being non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr
for x being Element of L
for m being Element of NAT st x <> 0. L & x |^ m = 1. L holds
(x ") |^ m = 1. L
Lm11:
for L being non empty non degenerated almost_left_invertible well-unital distributive associative commutative doubleLoopStr
for x being Element of L
for i being Element of NAT st x <> 0. L & (x ") |^ i = 1. L holds
x |^ i = 1. L
definition
let L be non
empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr ;
let m be
Nat;
let x be
Element of
L;
existence
ex b1 being Matrix of m,L st
for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds
b1 * (i,j) = pow (x,((i - 1) * (j - 1)))
uniqueness
for b1, b2 being Matrix of m,L st ( for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds
b1 * (i,j) = pow (x,((i - 1) * (j - 1))) ) & ( for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds
b2 * (i,j) = pow (x,((i - 1) * (j - 1))) ) holds
b1 = b2
end;
theorem Th35:
for
L being
Field for
m,
n being
Nat st
m > 0 holds
for
M being
Matrix of
m,
n,
L holds
(1. (L,m)) * M = M
Lm12:
for L being Field
for m being Element of NAT st m > 0 holds
for p, q being Polynomial of L holds (emb ((2 * m),L)) * ((1. (L,(2 * m))) * (mConv ((p *' q),(2 * m)))) = (emb ((2 * m),L)) * (mConv ((p *' q),(2 * m)))