FIELD_16: Finite Fields

proof end;

end;

definition

let L1, L2 be non empty 1-sorted ;
let F be Funcs (L1,L2) -valued sequence ;
let n be Nat;
:: original: .
redefine func F . n -> Function of L1,L2;
coherence

proof end;

end;

registration

let F be Field;

cluster non empty trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable Abelian add-associative right_zeroed zeroed vector-distributive scalar-distributive scalar-associative scalar-unital left_zeroed add-left-invertible add-right-invertible Loop-like for ModuleStr over F;

proof end;

end;

scheme :: FIELD_16:sch 1
RecExF{ F₁() -> non empty 1-sorted , F₂() -> Function of F₁(),F₁(), P₁[ object , Function of F₁(),F₁(), Function of F₁(),F₁()] } :

ex f being Funcs (F₁(),F₁()) -valued sequence st
( f . 0 = F₂() & ( for n being Nat holds P₁[n,f . n,f . (n + 1)] ) )

provided

A1: for n being Nat
for g1 being Function of F₁(),F₁() ex g2 being Function of F₁(),F₁() st P₁[n,g1,g2]

proof end;

definition

let L be non empty 1-sorted ;
let f be Function of L,L;
let n be Nat;

func f `^ n -> Function of L,L means :dd: :: FIELD_16:def 1
ex F being Funcs (L,L) -valued sequence st
( it = F . n & F . 0 = id L & ( for i being Nat holds F . (i + 1) = (F . i) * f ) );

proof end;

uniqueness

proof end;

end;

:: deftheorem dd defines `^ FIELD_16:def 1 :

registration

let L be non empty 1-sorted ;
let f be Function of L,L;

reduce f `^ 1 to f;

reducibility

proof end;

end;

theorem T1: :: FIELD_16:1

for L being non empty 1-sorted
for f being Function of L,L holds
( f `^ 0 = id L & f `^ 1 = f & f `^ 2 = f * f )

proof end;

theorem T3: :: FIELD_16:2

for L being non empty 1-sorted
for f being Function of L,L
for n being Nat holds
( f `^ (n + 1) = (f `^ n) * f & (f `^ n) * f = f * (f `^ n) )

proof end;

registration

let L be non empty 1-sorted ;
let n be Nat;

reduce (id L) `^ n to id L;

reducibility

proof end;

end;

theorem lemf: :: FIELD_16:3

for L being non empty 1-sorted
for f being Function of L,L
for n, m being Nat holds f `^ (n + m) = (f `^ n) * (f `^ m)

proof end;

theorem :: FIELD_16:4

for L being non empty 1-sorted
for f being Function of L,L
for n, m being Nat holds f `^ (n * m) = (f `^ n) `^ m

proof end;

theorem TT2: :: FIELD_16:5

for L being non empty 1-sorted
for f being bijective Function of L,L
for n, m being Nat holds
( f `^ (n + 1) = f `^ (m + 1) iff f `^ n = f `^ m )

proof end;

theorem TT3: :: FIELD_16:6

for L being non empty 1-sorted
for f being bijective Function of L,L
for n, m, k being Nat st f `^ n = f `^ m & k = n - m holds
f `^ k = f `^ 0

proof end;

registration

let F be Field;

cluster Relation-like the carrier of F -defined the carrier of F -valued Function-like non empty total quasi_total isomorphism for Element of bool [: the carrier of F, the carrier of F:];

proof end;

end;

registration

let R be Ring;
let f, g be isomorphism Function of R,R;

cluster g * f -> isomorphism for Function of R,R;

proof end;

end;

registration

let R be Ring;
let f be isomorphism Function of R,R;
let n be Nat;

cluster f `^ n -> isomorphism for Function of R,R;

proof end;

end;

registration

let R be Ring;
let f be isomorphism Function of R,R;

cluster f " -> isomorphism for Function of R,R;

proof end;

end;

definition

let F be Field;
let S be Subset of F;

attr S is inducing_subfield means :IS: :: FIELD_16:def 2
( 0. F in S & 1. F in S & ( for a, b being Element of F st a in S & b in S holds
( a + b in S & a * b in S & - a in S ) ) & ( for a being non zero Element of F st a in S holds
a " in S ) );

end;

:: deftheorem IS defines inducing_subfield FIELD_16:def 2 :

registration

let F be Field;

cluster inducing_subfield for Element of bool the carrier of F;

proof end;

end;

registration

let F be Field;

cluster inducing_subfield -> non empty inducing_subfield for Element of bool the carrier of F;

coherence by IS;

end;

definition

let F be Field;
let S be inducing_subfield Subset of F;

func InducedSubfield S -> non empty strict doubleLoopStr means :dis: :: FIELD_16:def 3
( the carrier of it = S & the addF of it = the addF of F || S & the multF of it = the multF of F || S & 0. it = 0. F & 1. it = 1. F );

proof end;

uniqueness ;

end;

:: deftheorem dis defines InducedSubfield FIELD_16:def 3 :

registration

let F be Field;
let S be inducing_subfield Subset of F;

cluster InducedSubfield S -> non empty non degenerated strict ;

proof end;

end;

Lm11a: for F being Field
for S being inducing_subfield Subset of F
for a, b being Element of F
for x, y being Element of (InducedSubfield S) st a = x & b = y holds
( a + b = x + y & a * b = x * y )

proof end;

registration

let F be Field;
let S be inducing_subfield Subset of F;

cluster InducedSubfield S -> non empty right_complementable strict Abelian add-associative right_zeroed ;

proof end;

end;

registration

let F be Field;
let S be inducing_subfield Subset of F;

cluster InducedSubfield S -> non empty almost_left_invertible strict well-unital distributive associative commutative ;

proof end;

end;

definition

let F be Field;
let S be inducing_subfield Subset of F;
:: original: InducedSubfield
redefine func InducedSubfield S -> strict Subfield of F;
coherence

proof end;

end;

registration

let E be Field;
let F be Subfield of E;

cluster the carrier of F -> inducing_subfield for Subset of E;

proof end;

end;

registration

let F be Field;

cluster the carrier of F -> inducing_subfield for Subset of F;

end;

registration

let R1 be Ring;
let R2 be R1 -isomorphic Ring;
let R3 be R2 -isomorphic Ring;
let f be Isomorphism of R1,R2;
let g be Isomorphism of R2,R3;

cluster f * g -> isomorphism for Function of R1,R3;

proof end;

end;

registration

let F be Field;
let E be FieldExtension of F;
let f be additive Function of E,E;

cluster f | the carrier of F -> additive for Function of F,F;

proof end;

end;

registration

let F be Field;
let E be FieldExtension of F;
let f be multiplicative Function of E,E;

cluster f | the carrier of F -> multiplicative for Function of F,F;

proof end;

end;

registration

let F be Field;
let E be FieldExtension of F;
let f be unity-preserving Function of E,E;

cluster f | the carrier of F -> unity-preserving for Function of F,F;

proof end;

end;

definition

let n, m be Nat;

attr m is n -power means :defpower: :: FIELD_16:def 4
ex l being non zero Nat st m = n |^ l;

end;

:: deftheorem defpower defines -power FIELD_16:def 4 :

registration

let n be Nat;
let l be non zero Nat;

cluster n |^ l -> n -power ;

end;

registration

let n be Nat;

cluster epsilon-transitive epsilon-connected ordinal natural real finite cardinal complex integer dim-like ext-real non negative g_integer g_rational n -power for set ;

proof end;

end;

definition

let n be Nat;
mode Power of n is n -power Nat;

end;

registration

let n be non zero Nat;

cluster natural n -power -> non zero for set ;

proof end;

end;

registration

let n be non trivial Nat;

cluster natural n -power -> non trivial for set ;

proof end;

end;

thX3a: for a, b, n being Nat st a >= b holds
a |^ n >= b |^ n
by NEWTON02:41;

TT7: for a being non zero Nat
for n, m being Nat st n >= m holds
a |^ n >= a |^ m
by NAT_6:1;

theorem lemp: :: FIELD_16:7

for p1, p2 being Prime
for n1, n2 being Nat st ( n1 <> 0 or n2 <> 0 ) & p1 |^ n1 = p2 |^ n2 holds
( p1 = p2 & n1 = n2 )

proof end;

theorem F16: :: FIELD_16:8

for F being Field
for a being non zero Element of F
for n being Nat holds (a ") |^ n = (a |^ n) "

proof end;

theorem lemID: :: FIELD_16:9

for R being Ring
for S being b₁ -homomorphic Ring
for f being unity-preserving multiplicative Function of R,S
for a being Element of R
for n being Nat holds f . (a |^ n) = (f . a) |^ n

proof end;

registration

let R be Ring;
let p be Polynomial of R;

reduce - (- p) to p;

reducibility

proof end;

end;

theorem lemX: :: FIELD_16:10

for R being Ring
for p1, p2 being Polynomial of R holds p1 *' (- p2) = - (p1 *' p2)

proof end;

theorem ID2: :: FIELD_16:11

for R being domRing
for S being domRingExtension of R
for p being non zero Element of the carrier of (Polynom-Ring R) holds card (Roots (S,p)) <= deg p

proof end;

theorem ThA: :: FIELD_16:12

for F being Field
for E being FieldExtension of F
for a being Element of E
for n being Nat holds a |^ n in the carrier of (FAdj (F,{a}))

proof end;

theorem ID2a: :: FIELD_16:13

for F being Field
for E being FieldExtension of F
for a being b₁ -algebraic Element of E
for f being b₁ -fixing Automorphism of (FAdj (F,{a})) holds f . a in Roots ((FAdj (F,{a})),(MinPoly (a,F)))

proof end;

theorem FAutEQ1: :: FIELD_16:14

for F being Field
for E1, E2 being FieldExtension of F st E1 == E2 holds
for f being Automorphism of E1 holds f is Automorphism of E2

proof end;

theorem FAutEQ: :: FIELD_16:15

for F being Field
for E1, E2 being FieldExtension of F st E1 == E2 holds
{ f where f is Automorphism of E1 : verum } = { f where f is Automorphism of E2 : verum }

proof end;

theorem ID: :: FIELD_16:16

for F being Field
for E being FieldExtension of F
for a being b₁ -algebraic Element of E
for f, g being b₁ -fixing Automorphism of (FAdj (F,{a})) st f . a = g . a holds
f = g

proof end;

FAUTh: for F being Field
for E being FieldExtension of F
for a being b₁ -algebraic Element of E
for n being Nat st n = card { f where f is b₁ -fixing Automorphism of (FAdj (F,{a})) : verum } holds
n <= card (Roots ((FAdj (F,{a})),(MinPoly (a,F))))

proof end;

theorem FAUTfin: :: FIELD_16:17

for F being Field
for E being FieldExtension of F
for a being b₁ -algebraic Element of E holds { f where f is b₁ -fixing Automorphism of (FAdj (F,{a})) : verum } is finite

proof end;

theorem :: FIELD_16:18

for F being Field
for E being FieldExtension of F
for a being b₁ -algebraic Element of E holds card { f where f is b₁ -fixing Automorphism of (FAdj (F,{a})) : verum } c= card (Roots ((FAdj (F,{a})),(MinPoly (a,F))))

proof end;

theorem lemMA: :: FIELD_16:19

for F being Field
for E being FieldExtension of F
for p being non constant Element of the carrier of (Polynom-Ring F) holds
( card (Roots (E,p)) = deg p iff ( p splits_in E & p is separable ) )

proof end;

registration

let F be finite Field;

cluster -> finite for Subfield of F;

proof end;

end;

registration

let F be Field;
let K be FieldExtension of PrimeField F;

cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_cancelable almost_right_cancelable almost_cancelable almost_left_invertible almost_right_invertible almost_invertible Abelian add-associative right_zeroed zeroed right-distributive left-distributive right_unital well-unital distributive left_unital unital associative commutative left_zeroed add-left-invertible add-right-invertible Loop-like PID Euclidian PrimeField F -homomorphic factorial domRing-like PrimeField F -monomorphic K -extending PrimeField F -extending gcd-like for doubleLoopStr ;

proof end;

end;

notation

let F be finite Field;
synonym order F for card F;

end;

registration

let F be finite Field;

cluster order F -> natural ;

end;

registration

let F be finite Field;

cluster order F -> non trivial ;

proof end;

end;

registration

let F be finite Field;

cluster non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed well-unital distributive associative commutative F -extending F -finite -> finite F -finite for doubleLoopStr ;

proof end;

end;

registration

let F be finite Field;

proof end;

end;

definition

let R be Ring;

attr R is reduced means :NIL1: :: FIELD_16:def 5
for a being nilpotent Element of R holds a = 0. R;

end;

:: deftheorem NIL1 defines reduced FIELD_16:def 5 :

registration

let R be non degenerated commutative Ring;

cluster nilpotent -> non unital for Element of the carrier of R;

proof end;

end;

theorem :: FIELD_16:20

for R being non degenerated commutative Ring holds
( R is reduced iff nilrad R = {(0. R)} )

proof end;

registration

cluster non empty non degenerated right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative domRing-like -> reduced for doubleLoopStr ;

proof end;

end;

registration

let R be domRing;

cluster non zero -> non zero non nilpotent for Element of the carrier of R;

proof end;

end;

definition

let R be Ring;

func FrobeniusMorphism R -> Function of R,R means :defFr: :: FIELD_16:def 6
for a being Element of R holds it . a = a |^ (Char R);

proof end;

uniqueness

proof end;

end;

:: deftheorem defFr defines FrobeniusMorphism FIELD_16:def 6 :

notation

let R be Ring;
synonym Frob R for FrobeniusMorphism R;

end;

registration

let p be Prime;
let R be commutative p -characteristic Ring;

cluster FrobeniusMorphism R -> additive unity-preserving multiplicative ;

proof end;

end;

theorem FrK: :: FIELD_16:21

for n being Nat
for R being b₁ -characteristic Ring holds ker (Frob R) = { a where a is Element of R : a |^ n = 0. R }

proof end;

theorem :: FIELD_16:22

for R being non degenerated commutative Ring holds ker (Frob R) c= nilrad R

proof end;

theorem :: FIELD_16:23

for R being 0 -characteristic Ring holds Frob R = the carrier of R --> (1. R)

proof end;

T4: for R being Ring
for a being Element of R
for n being Nat holds ((Frob R) `^ n) . a = a |^ ((Char R) |^ n)

proof end;

theorem fresh3a: :: FIELD_16:24

for p being Prime holds card (Z/ p) = p

proof end;

theorem fresh3: :: FIELD_16:25

for p being Prime
for a being Element of (Z/ p) holds a |^ p = a

proof end;

theorem :: FIELD_16:26

for p being Prime holds Frob (Z/ p) = id (Z/ p)

proof end;

theorem T5: :: FIELD_16:27

for p being Prime
for n being non zero Nat
for F being Field st card F = p |^ n holds
Char F = p

proof end;

theorem thX0: :: FIELD_16:28

for p being Prime
for n being non zero Nat
for F being Field st card F = p |^ n holds
for a being Element of F holds a |^ (p |^ n) = a

proof end;

registration

let p be Prime;
let R be commutative p -characteristic reduced Ring;

cluster FrobeniusMorphism R -> one-to-one ;

proof end;

end;

registration

let F be finite Field;

cluster FrobeniusMorphism F -> onto ;

proof end;

end;

theorem :: FIELD_16:29

for p being Prime
for F being b₁ -characteristic Field holds
( F is perfect iff Frob F is Automorphism of F )

proof end;

Lm10: for L being non empty unital doubleLoopStr
for n being non trivial Nat holds
( ((0_. L) +* ((1,n) --> ((- (1. L)),(1. L)))) . 1 = - (1. L) & ((0_. L) +* ((1,n) --> ((- (1. L)),(1. L)))) . n = 1. L )

proof end;

Lm11: for L being non empty unital doubleLoopStr
for i, n being Nat st i <> 1 & i <> n holds
((0_. L) +* ((1,n) --> ((- (1. L)),(1. L)))) . i = 0. L

proof end;

definition

let R be non empty unital doubleLoopStr ;
let n be non trivial Nat;

func X^ (n,R) -> sequence of R equals :: FIELD_16:def 7
(0_. R) +* ((1,n) --> ((- (1. R)),(1. R)));

proof end;

end;

:: deftheorem defines X^ FIELD_16:def 7 :

registration

let R be non empty unital doubleLoopStr ;
let n be non trivial Nat;

cluster X^ (n,R) -> finite-Support ;

end;

Lm12: for R being non degenerated unital doubleLoopStr
for n being non trivial Nat holds deg (X^ (n,R)) = n

proof end;

Lm13: for R being non degenerated unital doubleLoopStr
for n being non trivial Nat holds LC (X^ (n,R)) = 1. R

proof end;

registration

let R be non degenerated Ring;
let n be non trivial Nat;

cluster X^ (n,R) -> non constant monic ;

proof end;

end;

definition

let R be non degenerated Ring;
let n be non trivial Nat;
:: original: X^
redefine func X^ (n,R) -> non constant Element of the carrier of (Polynom-Ring R);
coherence

proof end;

end;

theorem :: FIELD_16:30

for R being non degenerated unital doubleLoopStr
for a being Element of R
for n being non trivial Nat holds
( (X^ (n,R)) . 1 = - (1. R) & (X^ (n,R)) . n = 1. R & ( for m being Nat st m <> 1 & m <> n holds
(X^ (n,R)) . m = 0. R ) ) by Lm10, Lm11;

theorem :: FIELD_16:31

for R being non degenerated unital doubleLoopStr
for n being non trivial Nat holds deg (X^ (n,R)) = n by Lm12;

theorem :: FIELD_16:32

for R being non degenerated unital doubleLoopStr
for n being non trivial Nat holds LC (X^ (n,R)) = 1. R by Lm13;

theorem teval: :: FIELD_16:33

for R being non degenerated Ring
for n being non trivial Nat
for a being Element of R holds eval ((X^ (n,R)),a) = (a |^ n) - a

proof end;

theorem thXX: :: FIELD_16:34

for R being non degenerated unital Ring
for n being non trivial Nat
for a being Element of R holds
( a is_a_root_of X^ (n,R) iff a |^ n = a )

proof end;

theorem thX1: :: FIELD_16:35

for p being Prime
for n being non zero Nat
for F being b₁ -characteristic Field st card F = p |^ n holds
for a being Element of F holds eval ((X^ ((p |^ n),F)),a) = 0. F

proof end;

theorem tevale: :: FIELD_16:36

for R being non degenerated Ring
for S being RingExtension of R
for n being non trivial Nat
for a being Element of S holds Ext_eval ((X^ (n,R)),a) = (a |^ n) - a

proof end;

theorem thXXe: :: FIELD_16:37

for R being non degenerated unital Ring
for S being RingExtension of R
for n being non trivial Nat
for a being Element of S holds
( a is_a_root_of X^ (n,R),S iff a |^ n = a )

proof end;

thX1e: for p being Prime
for n being non zero Nat
for F being b₁ -characteristic Field
for E being FieldExtension of F st card E = p |^ n holds
for a being Element of E holds Ext_eval ((X^ ((p |^ n),F)),a) = 0. E

proof end;

theorem :: FIELD_16:38

for p being Prime
for R being commutative b₁ -characteristic Ring
for n being non zero Nat holds { (m * (1. R)) where m is Nat : m < p } c= Roots (X^ ((p |^ n),R))

proof end;

theorem thX1ee: :: FIELD_16:39

for p being Prime
for n being non zero Nat
for F being b₁ -characteristic Field st card F = p |^ n holds
Roots (X^ ((p |^ n),F)) = the carrier of F

proof end;

theorem thX3: :: FIELD_16:40

for p being Prime
for n being non zero Nat
for F being b₁ -characteristic Field holds (Deriv F) . (X^ ((p |^ n),F)) = - (1_. F)

proof end;

theorem Xm: :: FIELD_16:41

for n being non trivial Nat
for R being Ring
for S being RingExtension of R holds X^ (n,R) = X^ (n,S)

proof end;

registration

let p be Prime;
let n be non zero Nat;
let F be p -characteristic Field;

cluster X^ ((p |^ n),F) -> non constant separable for non constant Element of the carrier of (Polynom-Ring F);

proof end;

end;

registration

let F be finite Field;

cluster X^ ((order F),F) -> non constant separable for non constant Element of the carrier of (Polynom-Ring F);

proof end;

end;

Ffix1: for p being Prime
for n being non zero Nat
for F being Field st card F = p |^ n holds
card (PrimeField F) = p

proof end;

finex2: for F being finite Field ex p being Prime ex n being non zero Nat st
( Char F = p & order F = p |^ n )

proof end;

theorem FFF: :: FIELD_16:42

for F being finite Field holds card (PrimeField F) = Char F

proof end;

FF: for p being Prime
for n being non zero Nat
for F being Field st card F = p |^ n holds
Roots (X^ (p,F)) = the carrier of (PrimeField F)

proof end;

theorem :: FIELD_16:43

for F being finite Field holds Roots (X^ ((Char F),F)) = the carrier of (PrimeField F)

proof end;

Ffix2: for p being Prime
for n being non zero Nat
for F being Field st card F = p |^ n holds
for a being Element of F holds
( (Frob F) . a = a iff a in PrimeField F )

proof end;

theorem FA2: :: FIELD_16:44

for p being Prime
for n being non zero Nat
for F being Field st card F = p |^ n holds
card (PrimeField F) = p

proof end;

theorem :: FIELD_16:45

for F being finite Field
for a being Element of F holds
( (Frob F) . a = a iff a in PrimeField F )

proof end;

theorem fresh3P: :: FIELD_16:46

for p being Prime
for n being non zero Nat
for F being Field st card F = p |^ n holds
for a being Element of F holds
( a in PrimeField F iff a |^ p = a )

proof end;

theorem FA4a: :: FIELD_16:47

for F being finite Field
for f being Automorphism of F
for a being Element of F holds
( f . a in PrimeField F iff a in PrimeField F )

proof end;

theorem PrimAUT: :: FIELD_16:48

for F being prime Field
for f being Automorphism of F holds f = id F

proof end;

theorem FA4: :: FIELD_16:49

for F being finite Field
for f being Automorphism of F
for a being Element of (PrimeField F) holds f . a = a

proof end;

theorem FA3: :: FIELD_16:50

for p being Prime
for n being non zero Nat
for F being Field
for E being FieldExtension of F st card E = p |^ n & F == PrimeField E holds
deg (E,F) = n

proof end;

theorem FA1: :: FIELD_16:51

for F being finite Field holds F is PrimeField b₁ -finite FieldExtension of PrimeField F

proof end;

theorem :: FIELD_16:52

for F being finite Field holds F is PrimeField b₁ -simple FieldExtension of PrimeField F by FA1;

registration

let p be Prime;
let n be non zero Nat;
let F be p -characteristic Field;

cluster Roots (X^ ((p |^ n),F)) -> inducing_subfield ;

proof end;

end;

registration

let p be Prime;
let n be non zero Nat;
let F be p -characteristic Field;
let E be SplittingField of X^ ((p |^ n),(PrimeField F));

cluster Roots (E,(X^ ((p |^ n),(PrimeField F)))) -> inducing_subfield ;

proof end;

end;

theorem lemex: :: FIELD_16:53

for p being Prime
for n being non zero Nat
for F being b₁ -characteristic Field
for E being SplittingField of X^ ((p |^ n),(PrimeField F)) holds card (Roots (E,(X^ ((p |^ n),(PrimeField F))))) = p |^ n

proof end;

theorem :: FIELD_16:54

for p being Prime
for n being non zero Nat
for F being b₁ -characteristic Field
for E being SplittingField of X^ ((p |^ n),(PrimeField F)) holds E == InducedSubfield (Roots (E,(X^ ((p |^ n),(PrimeField F)))))

proof end;

theorem split: :: FIELD_16:55

for p being Prime
for n being non zero Nat
for F being Field st card F = p |^ n holds
F is SplittingField of X^ ((p |^ n),(PrimeField F))

proof end;

theorem :: FIELD_16:56

for p being Prime
for n being non zero Nat
for F being finite Field st card F = p |^ n holds
X^ ((p |^ n),F) is Ppoly of F,([#] the carrier of F)

proof end;

theorem :: FIELD_16:57

for p being Prime
for n being non zero Nat ex F being finite Field st
( Char F = p & order F = p |^ n )

proof end;

theorem :: FIELD_16:58

for F being finite Field ex p being Prime ex n being non zero Nat st
( Char F = p & order F = p |^ n ) by finex2;

theorem finun: :: FIELD_16:59

for F1, F2 being finite Field st order F1 = order F2 holds
F1,F2 are_isomorphic

proof end;

theorem ThNS: :: FIELD_16:60

for F being finite Field holds F is PrimeField b₁ -normal PrimeField b₁ -separable FieldExtension of PrimeField F

proof end;

registration

let F be finite Field;
let n be Nat;

cluster (Frob F) `^ n -> isomorphism ;

proof end;

end;

registration

let F be finite Field;

cluster FrobeniusMorphism F -> isomorphism ;