let F be commutative Skew-Field; :: thesis: for G being Subgroup of MultGroup F
for n being Nat st 0 < n holds
ex f being Polynomial of F st
( deg f = n & ( for x, xn being Element of F
for xz being Element of G st x = xz & xn = xz |^ n holds
eval f,x = xn - (1. F) ) )
let G be Subgroup of MultGroup F; :: thesis: for n being Nat st 0 < n holds
ex f being Polynomial of F st
( deg f = n & ( for x, xn being Element of F
for xz being Element of G st x = xz & xn = xz |^ n holds
eval f,x = xn - (1. F) ) )
let n be Nat; :: thesis: ( 0 < n implies ex f being Polynomial of F st
( deg f = n & ( for x, xn being Element of F
for xz being Element of G st x = xz & xn = xz |^ n holds
eval f,x = xn - (1. F) ) ) )
assume
0 < n
; :: thesis: ex f being Polynomial of F st
( deg f = n & ( for x, xn being Element of F
for xz being Element of G st x = xz & xn = xz |^ n holds
eval f,x = xn - (1. F) ) )
then A1:
0 + 1 < n + 1
by XREAL_1:10;
reconsider n0 = n as Element of NAT by ORDINAL1:def 13;
set f = (<%(0. F),(1_ F)%> `^ n0) - (1_. F);
A2:
now let x,
xn be
Element of
F;
:: thesis: for xz being Element of G st x = xz & xn = xz |^ n holds
eval ((<%(0. F),(1_ F)%> `^ n0) - (1_. F)),x = xn - (1_ F)let xz be
Element of
G;
:: thesis: ( x = xz & xn = xz |^ n implies eval ((<%(0. F),(1_ F)%> `^ n0) - (1_. F)),x = xn - (1_ F) )assume A3:
(
x = xz &
xn = xz |^ n )
;
:: thesis: eval ((<%(0. F),(1_ F)%> `^ n0) - (1_. F)),x = xn - (1_ F)
the
carrier of
G c= the
carrier of
(MultGroup F)
by GROUP_2:def 5;
then reconsider xxz =
xz as
Element of
(MultGroup F) by TARSKI:def 3;
A4:
xn =
xxz |^ n0
by GROUP_4:3, A3
.=
(power F) . x,
n0
by UNIROOTS:32, A3
;
thus eval ((<%(0. F),(1_ F)%> `^ n0) - (1_. F)),
x =
(eval (<%(0. F),(1_ F)%> `^ n0),x) - (eval (1_. F),x)
by POLYNOM4:24
.=
(eval (<%(0. F),(1_ F)%> `^ n0),x) - (1_ F)
by POLYNOM4:21
.=
((power F) . (eval <%(0. F),(1_ F)%>,x),n0) - (1_ F)
by POLYNOM5:23
.=
xn - (1_ F)
by A4, POLYNOM5:49
;
:: thesis: verum end;
A5:
len <%(0. F),(1_ F)%> = 2
by POLYNOM5:41;
A6: len (<%(0. F),(1_ F)%> `^ n0) =
((n * 2) - n) + 1
by A5, POLYNOM5:24
.=
n + 1
;
len (1_. F) = 1
by POLYNOM4:7;
then A7:
len (- (1_. F)) = 1
by POLYNOM4:11;
len ((<%(0. F),(1_ F)%> `^ n0) - (1_. F)) =
max (n + 1),1
by A6, A7, POLYNOM4:10, A1
.=
n + 1
by XXREAL_0:def 10, A1
;
then
deg ((<%(0. F),(1_ F)%> `^ n0) - (1_. F)) = n
;
hence
ex f being Polynomial of F st
( deg f = n & ( for x, xn being Element of F
for xz being Element of G st x = xz & xn = xz |^ n holds
eval f,x = xn - (1. F) ) )
by A2; :: thesis: verum