let F be commutative Skew-Field; 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; 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; ( 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) ) ) )
reconsider n0 = n as Element of NAT by ORDINAL1:def 12;
set f = (<%(0. F),(1_ F)%> `^ n0) - (1_. F);
A1:
now for x, xn being Element of F
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 x,
xn be
Element of
F;
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;
( x = xz & xn = xz |^ n implies eval (((<%(0. F),(1_ F)%> `^ n0) - (1_. F)),x) = xn - (1_ F) )assume that A2:
x = xz
and A3:
xn = xz |^ n
;
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) ;
A4:
xn =
xxz |^ n0
by A3, GROUP_4:1
.=
(power F) . (
x,
n0)
by A2, UNIROOTS:29
;
thus eval (
((<%(0. F),(1_ F)%> `^ n0) - (1_. F)),
x) =
(eval ((<%(0. F),(1_ F)%> `^ n0),x)) - (eval ((1_. F),x))
by POLYNOM4:21
.=
(eval ((<%(0. F),(1_ F)%> `^ n0),x)) - (1_ F)
by POLYNOM4:18
.=
((power F) . ((eval (<%(0. F),(1_ F)%>,x)),n0)) - (1_ F)
by POLYNOM5:22
.=
xn - (1_ F)
by A4, POLYNOM5:48
;
verum end;
assume
0 < n
; 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 A5:
0 + 1 < n + 1
by XREAL_1:8;
len (1_. F) = 1
by POLYNOM4:4;
then A6:
len (- (1_. F)) = 1
by POLYNOM4:8;
len <%(0. F),(1_ F)%> = 2
by POLYNOM5:40;
then len (<%(0. F),(1_ F)%> `^ n0) =
((n * 2) - n) + 1
by POLYNOM5:23
.=
n + 1
;
then len ((<%(0. F),(1_ F)%> `^ n0) - (1_. F)) =
max ((n + 1),1)
by A5, A6, POLYNOM4:7
.=
n + 1
by A5, XXREAL_0:def 10
;
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 A1; verum