:: Characteristic of Rings; Prime Fields
:: by Christoph Schwarzweller and Artur Korni{\l}owicz
::
:: Copyright (c) 2015-2021 Association of Mizar Users

theorem Th1: :: RING_3:1
for f being Function
for A being set
for a, b being object st a in A & b in A holds
(f || A) . (a,b) = f . (a,b)
proof end;

theorem Th2: :: RING_3:2
proof end;

theorem Th3: :: RING_3:3
proof end;

theorem Th4: :: RING_3:4
proof end;

theorem Th5: :: RING_3:5
proof end;

theorem Th6: :: RING_3:6
for n being Nat
for i being Integer st n divides i holds
i div n = i / n
proof end;

theorem Th7: :: RING_3:7
for n being Nat
for i being Integer holds i div (i gcd n) = i / (i gcd n)
proof end;

theorem Th8: :: RING_3:8
for n being Nat
for i being Integer holds n div (n gcd i) = n / (n gcd i)
proof end;

theorem Th9: :: RING_3:9
for g, m being Nat
for i being Integer st g divides i & g divides m holds
i / m = (i div g) / (m div g)
proof end;

theorem Th10: :: RING_3:10
for m being Nat
for i being Integer holds i / m = (i div (i gcd m)) / (m div (i gcd m))
proof end;

theorem Th11: :: RING_3:11
for m being Nat
for i being Integer st 0 < m & m * i divides m & not i = 1 holds
i = - 1
proof end;

theorem :: RING_3:12
for m, n being Nat st 0 < m & m * n divides m holds
n = 1
proof end;

theorem :: RING_3:13
for m being Nat
for i being Integer st m divides i holds
i div m divides i
proof end;

theorem Th14: :: RING_3:14
for m being Nat
for i being Integer st m <> 0 holds
(i div (i gcd m)) gcd (m div (i gcd m)) = 1
proof end;

theorem Th15: :: RING_3:15
for m being Nat
for i being Integer st m <> 0 holds
( denominator (i / m) = m div (i gcd m) & numerator (i / m) = i div (i gcd m) )
proof end;

theorem :: RING_3:16
for m being Nat
for i being Integer st m <> 0 holds
( denominator (i / m) = m / (i gcd m) & numerator (i / m) = i / (i gcd m) )
proof end;

theorem Th17: :: RING_3:17
for m being Nat
for i being Integer st m <> 0 holds
( denominator (- (i / m)) = m div ((- i) gcd m) & numerator (- (i / m)) = (- i) div ((- i) gcd m) )
proof end;

theorem :: RING_3:18
for m being Nat
for i being Integer st m <> 0 holds
( denominator (- (i / m)) = m / ((- i) gcd m) & numerator (- (i / m)) = (- i) / ((- i) gcd m) )
proof end;

theorem Th19: :: RING_3:19
for m being Nat
for i being Integer st m <> 0 holds
( denominator ((m / i) ") = m div (m gcd i) & numerator ((m / i) ") = i div (m gcd i) )
proof end;

theorem :: RING_3:20
for m being Nat
for i being Integer st m <> 0 holds
( denominator ((m / i) ") = m / (m gcd i) & numerator ((m / i) ") = i / (m gcd i) )
proof end;

theorem Th21: :: RING_3:21
for m, n being Nat
for i, j being Integer st m <> 0 & n <> 0 holds
( denominator ((i / m) + (j / n)) = (m * n) div (((i * n) + (j * m)) gcd (m * n)) & numerator ((i / m) + (j / n)) = ((i * n) + (j * m)) div (((i * n) + (j * m)) gcd (m * n)) )
proof end;

theorem :: RING_3:22
for m, n being Nat
for i, j being Integer st m <> 0 & n <> 0 holds
( denominator ((i / m) + (j / n)) = (m * n) / (((i * n) + (j * m)) gcd (m * n)) & numerator ((i / m) + (j / n)) = ((i * n) + (j * m)) / (((i * n) + (j * m)) gcd (m * n)) )
proof end;

theorem Th23: :: RING_3:23
for m, n being Nat
for i, j being Integer st m <> 0 & n <> 0 holds
( denominator ((i / m) - (j / n)) = (m * n) div (((i * n) - (j * m)) gcd (m * n)) & numerator ((i / m) - (j / n)) = ((i * n) - (j * m)) div (((i * n) - (j * m)) gcd (m * n)) )
proof end;

theorem :: RING_3:24
for m, n being Nat
for i, j being Integer st m <> 0 & n <> 0 holds
( denominator ((i / m) - (j / n)) = (m * n) / (((i * n) - (j * m)) gcd (m * n)) & numerator ((i / m) - (j / n)) = ((i * n) - (j * m)) / (((i * n) - (j * m)) gcd (m * n)) )
proof end;

theorem Th25: :: RING_3:25
for m, n being Nat
for i, j being Integer st m <> 0 & n <> 0 holds
( denominator ((i / m) * (j / n)) = (m * n) div ((i * j) gcd (m * n)) & numerator ((i / m) * (j / n)) = (i * j) div ((i * j) gcd (m * n)) )
proof end;

theorem :: RING_3:26
for m, n being Nat
for i, j being Integer st m <> 0 & n <> 0 holds
( denominator ((i / m) * (j / n)) = (m * n) / ((i * j) gcd (m * n)) & numerator ((i / m) * (j / n)) = (i * j) / ((i * j) gcd (m * n)) )
proof end;

theorem Th27: :: RING_3:27
for m, n being Nat
for i, j being Integer st m <> 0 & n <> 0 holds
( denominator ((i / m) / (n / j)) = (m * n) div ((i * j) gcd (m * n)) & numerator ((i / m) / (n / j)) = (i * j) div ((i * j) gcd (m * n)) )
proof end;

theorem :: RING_3:28
for m, n being Nat
for i, j being Integer st m <> 0 & n <> 0 holds
( denominator ((i / m) / (n / j)) = (m * n) / ((i * j) gcd (m * n)) & numerator ((i / m) / (n / j)) = (i * j) / ((i * j) gcd (m * n)) )
proof end;

theorem :: RING_3:29
for p being Rational holds denominator p = () div (() gcd ())
proof end;

theorem :: RING_3:30
for p being Rational holds numerator p = () div (() gcd ())
proof end;

theorem Th31: :: RING_3:31
for p being Rational
for m being Nat
for i being Integer st m = denominator p & i = numerator p holds
( denominator (- p) = m div ((- i) gcd m) & numerator (- p) = (- i) div ((- i) gcd m) )
proof end;

theorem :: RING_3:32
for p being Rational
for m being Nat
for i being Integer st m = denominator p & i = numerator p holds
( denominator (- p) = m / ((- i) gcd m) & numerator (- p) = (- i) / ((- i) gcd m) )
proof end;

theorem Th33: :: RING_3:33
for p being Rational
for m, n being Nat st m = denominator p & n = numerator p & n <> 0 holds
( denominator (p ") = n div (n gcd m) & numerator (p ") = m div (n gcd m) )
proof end;

theorem :: RING_3:34
for p being Rational
for m, n being Nat st m = denominator p & n = numerator p & n <> 0 holds
( denominator (p ") = n / (n gcd m) & numerator (p ") = m / (n gcd m) )
proof end;

theorem Th35: :: RING_3:35
for p, q being Rational
for m, n being Nat
for i, j being Integer st m = denominator p & n = denominator q & i = numerator p & j = numerator q holds
( denominator (p + q) = (m * n) div (((i * n) + (j * m)) gcd (m * n)) & numerator (p + q) = ((i * n) + (j * m)) div (((i * n) + (j * m)) gcd (m * n)) )
proof end;

theorem :: RING_3:36
for p, q being Rational
for m, n being Nat
for i, j being Integer st m = denominator p & n = denominator q & i = numerator p & j = numerator q holds
( denominator (p + q) = (m * n) / (((i * n) + (j * m)) gcd (m * n)) & numerator (p + q) = ((i * n) + (j * m)) / (((i * n) + (j * m)) gcd (m * n)) )
proof end;

theorem Th37: :: RING_3:37
for p, q being Rational
for m, n being Nat
for i, j being Integer st m = denominator p & n = denominator q & i = numerator p & j = numerator q holds
( denominator (p - q) = (m * n) div (((i * n) - (j * m)) gcd (m * n)) & numerator (p - q) = ((i * n) - (j * m)) div (((i * n) - (j * m)) gcd (m * n)) )
proof end;

theorem :: RING_3:38
for p, q being Rational
for m, n being Nat
for i, j being Integer st m = denominator p & n = denominator q & i = numerator p & j = numerator q holds
( denominator (p - q) = (m * n) / (((i * n) - (j * m)) gcd (m * n)) & numerator (p - q) = ((i * n) - (j * m)) / (((i * n) - (j * m)) gcd (m * n)) )
proof end;

theorem Th39: :: RING_3:39
for p, q being Rational
for m, n being Nat
for i, j being Integer st m = denominator p & n = denominator q & i = numerator p & j = numerator q holds
( denominator (p * q) = (m * n) div ((i * j) gcd (m * n)) & numerator (p * q) = (i * j) div ((i * j) gcd (m * n)) )
proof end;

theorem :: RING_3:40
for p, q being Rational
for m, n being Nat
for i, j being Integer st m = denominator p & n = denominator q & i = numerator p & j = numerator q holds
( denominator (p * q) = (m * n) / ((i * j) gcd (m * n)) & numerator (p * q) = (i * j) / ((i * j) gcd (m * n)) )
proof end;

theorem Th41: :: RING_3:41
for p, q being Rational
for m1, m2, n1, n2 being Nat st m1 = denominator p & m2 = denominator q & n1 = numerator p & n2 = numerator q & n2 <> 0 holds
( denominator (p / q) = (m1 * n2) div ((n1 * m2) gcd (m1 * n2)) & numerator (p / q) = (n1 * m2) div ((n1 * m2) gcd (m1 * n2)) )
proof end;

theorem :: RING_3:42
for p, q being Rational
for m1, m2, n1, n2 being Nat st m1 = denominator p & m2 = denominator q & n1 = numerator p & n2 = numerator q & n2 <> 0 holds
( denominator (p / q) = (m1 * n2) / ((n1 * m2) gcd (m1 * n2)) & numerator (p / q) = (n1 * m2) / ((n1 * m2) gcd (m1 * n2)) )
proof end;

set I = INT.Ring ;

registration
existence
ex b1 being Element of INT.Ring st b1 is positive
;
existence
ex b1 being Element of INT.Ring st b1 is negative
proof end;
end;

registration
let a be non zero Element of F_Rat;
let x be Rational;
identify / a with x " when a = x;
compatibility
( a = x implies / a = x " )
proof end;
end;

registration
let a be Element of F_Rat;
let b be non zero Element of F_Rat;
let x, y be Rational;
identify a / b with x / y when a = x, b = y;
compatibility
( a = x & b = y implies a / b = x / y )
;
end;

registration
let F be Field;
reduce (1. F) " to 1. F;
reducibility
(1. F) " = 1. F
by EC_PF_2:2;
end;

definition
let R, S be Ring;
pred R includes_an_isomorphic_copy_of S means :: RING_3:def 1
ex T being strict Subring of R st T,S are_isomorphic ;
end;

:: deftheorem defines includes_an_isomorphic_copy_of RING_3:def 1 :
for R, S being Ring holds
( R includes_an_isomorphic_copy_of S iff ex T being strict Subring of R st T,S are_isomorphic );

notation
let R, S be Ring;
synonym R includes S for R includes_an_isomorphic_copy_of S;
end;

definition
let R, S be Ring;
:: original: is_ringisomorph_to
redefine pred R,S are_isomorphic ;
reflexivity
for R being Ring holds R24(b1,b1)
proof end;
end;

theorem Lm1: :: RING_3:43
for E being Field
for F being Subfield of E holds F is Subring of E
proof end;

theorem Th43: :: RING_3:44
for R, S, T being Ring st R,S are_isomorphic & S,T are_isomorphic holds
R,T are_isomorphic
proof end;

theorem :: RING_3:45
for F being Field
for R being Subring of F holds
( R is Subfield of F iff R is Field )
proof end;

theorem :: RING_3:46
for E being Field
for F being strict Subfield of E holds E includes F
proof end;

Lm2: ( the carrier of F_Real is Subset of the carrier of F_Complex & the addF of F_Real = the addF of F_Complex || the carrier of F_Real & the multF of F_Real = the multF of F_Complex || the carrier of F_Real & 1. F_Complex = 1. F_Real & 0. F_Complex = 0. F_Real )
by ;

Lm3: for u, v being Integer
for p, q being Element of INT.Ring st u = p & v = q holds
( u divides v iff p divides q )

proof end;

Lm4: ( the carrier of INT.Ring c= the carrier of F_Rat & the addF of INT.Ring = the addF of F_Rat || the carrier of INT.Ring & the multF of INT.Ring = the multF of F_Rat || the carrier of INT.Ring & 1. INT.Ring = 1. F_Rat & 0. INT.Ring = 0. F_Rat )
by ;

theorem :: RING_3:47
INT.Ring is Subring of F_Rat by ;

theorem Th47: :: RING_3:48
F_Real is Subfield of F_Complex by ;

registration
let R be domRing;
existence
ex b1 being domRing st b1 is R -homomorphic
proof end;
existence
ex b1 being comRing st b1 is R -homomorphic
proof end;
existence
ex b1 being Ring st b1 is R -homomorphic
proof end;
end;

registration
let R be Field;
existence
ex b1 being domRing st b1 is R -homomorphic
proof end;
end;

registration
let F be Field;
let R be F -homomorphic Ring;
let f be Homomorphism of F,R;
coherence
proof end;
end;

registration
let F be domRing;
let E be F -homomorphic domRing;
let f be Homomorphism of F,E;
cluster Image f -> non degenerated ;
coherence
not Image f is degenerated
proof end;
end;

theorem Th48: :: RING_3:49
for R being Ring
for E being b1 -homomorphic Ring
for K being Subring of R
for f being Function of R,E
for g being Function of K,E st g = f | the carrier of K & f is additive holds
proof end;

theorem Th49: :: RING_3:50
for R being Ring
for E being b1 -homomorphic Ring
for K being Subring of R
for f being Function of R,E
for g being Function of K,E st g = f | the carrier of K & f is multiplicative holds
g is multiplicative
proof end;

theorem Th50: :: RING_3:51
for R being Ring
for E being b1 -homomorphic Ring
for K being Subring of R
for f being Function of R,E
for g being Function of K,E st g = f | the carrier of K & f is unity-preserving holds
g is unity-preserving
proof end;

theorem :: RING_3:52
for R being Ring
for E being b1 -homomorphic Ring
for K being Subring of R holds E is K -homomorphic
proof end;

theorem :: RING_3:53
for R being Ring
for E being b1 -homomorphic Ring
for K being Subring of R
for EK being b3 -homomorphic Ring
for f being Homomorphism of R,E st E = EK holds
f | K is Homomorphism of K,EK
proof end;

theorem Th53: :: RING_3:54
for F being Field
for E being b1 -homomorphic Field
for K being Subfield of F
for f being Function of F,E
for g being Function of K,E st g = f | the carrier of K & f is additive holds
proof end;

theorem Th54: :: RING_3:55
for F being Field
for E being b1 -homomorphic Field
for K being Subfield of F
for f being Function of F,E
for g being Function of K,E st g = f | the carrier of K & f is multiplicative holds
g is multiplicative
proof end;

theorem Th55: :: RING_3:56
for F being Field
for E being b1 -homomorphic Field
for K being Subfield of F
for f being Function of F,E
for g being Function of K,E st g = f | the carrier of K & f is unity-preserving holds
g is unity-preserving
proof end;

theorem Th56: :: RING_3:57
for F being Field
for E being b1 -homomorphic Field
for K being Subfield of F holds E is K -homomorphic
proof end;

theorem Th57: :: RING_3:58
for F being Field
for E being b1 -homomorphic Field
for K being Subfield of F
for EK being b3 -homomorphic Field
for f being Homomorphism of F,E st E = EK holds
f | K is Homomorphism of K,EK
proof end;

notation
let n be Nat;
synonym Z/ n for INT.Ring n;
end;

registration
let n be Nat;
cluster Z/ n -> finite ;
coherence
Z/ n is finite
;
end;

registration
let n be non trivial Nat;
cluster Z/ n -> non degenerated ;
coherence
not Z/ n is degenerated
proof end;
end;

registration
let n be positive Nat;
coherence
( Z/ n is Abelian & Z/ n is add-associative & Z/ n is right_zeroed & Z/ n is right_complementable )
proof end;
end;

registration
let n be positive Nat;
coherence
( Z/ n is associative & Z/ n is well-unital & Z/ n is distributive & Z/ n is commutative )
proof end;
end;

registration
let p be Prime;
coherence ;
end;

definition
let R be non empty right_complementable add-associative right_zeroed doubleLoopStr ;
let a be Element of R;
let i be Integer;
func i '*' a -> Element of R means :Def2: :: RING_3:def 2
ex n being Nat st
( ( i = n & it = n * a ) or ( i = - n & it = - (n * a) ) );
existence
ex b1 being Element of R ex n being Nat st
( ( i = n & b1 = n * a ) or ( i = - n & b1 = - (n * a) ) )
proof end;
uniqueness
for b1, b2 being Element of R st ex n being Nat st
( ( i = n & b1 = n * a ) or ( i = - n & b1 = - (n * a) ) ) & ex n being Nat st
( ( i = n & b2 = n * a ) or ( i = - n & b2 = - (n * a) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines '*' RING_3:def 2 :
for R being non empty right_complementable add-associative right_zeroed doubleLoopStr
for a being Element of R
for i being Integer
for b4 being Element of R holds
( b4 = i '*' a iff ex n being Nat st
( ( i = n & b4 = n * a ) or ( i = - n & b4 = - (n * a) ) ) );

theorem Th58: :: RING_3:59
for R being non empty right_complementable add-associative right_zeroed doubleLoopStr
for a being Element of R holds 0 '*' a = 0. R
proof end;

theorem Th59: :: RING_3:60
for R being non empty right_complementable add-associative right_zeroed doubleLoopStr
for a being Element of R holds 1 '*' a = a
proof end;

theorem Th60: :: RING_3:61
for R being non empty right_complementable add-associative right_zeroed doubleLoopStr
for a being Element of R holds (- 1) '*' a = - a
proof end;

Lm5: for R being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr
for a being Element of R
for i being Integer holds (i + 1) '*' a = (i '*' a) + a

proof end;

Lm6: for R being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr
for a being Element of R
for i being Integer holds (i - 1) '*' a = (i '*' a) - a

proof end;

theorem Th61: :: RING_3:62
for R being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr
for a being Element of R
for i, j being Integer holds (i + j) '*' a = (i '*' a) + (j '*' a)
proof end;

theorem Th62: :: RING_3:63
for R being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr
for a being Element of R
for i being Integer holds (- i) '*' a = - (i '*' a)
proof end;

theorem Th63: :: RING_3:64
for R being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr
for a being Element of R
for i, j being Integer holds (i - j) '*' a = (i '*' a) - (j '*' a)
proof end;

theorem Th64: :: RING_3:65
for R being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr
for a being Element of R
for i, j being Integer holds (i * j) '*' a = i '*' (j '*' a)
proof end;

theorem :: RING_3:66
for R being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr
for a being Element of R
for i, j being Integer holds i '*' (j '*' a) = j '*' (i '*' a)
proof end;

theorem Th66: :: RING_3:67
for R being non empty right_complementable Abelian add-associative right_zeroed distributive left_unital doubleLoopStr
for i, j being Integer holds (i * j) '*' (1. R) = (i '*' (1. R)) * (j '*' (1. R))
proof end;

theorem :: RING_3:68
for R being Ring
for S being b1 -homomorphic Ring
for f being Homomorphism of R,S
for a being Element of R
for i being Integer holds f . (i '*' a) = i '*' (f . a)
proof end;

definition
let R, S be Ring;
attr S is R -monomorphic means :Def3: :: RING_3:def 3
ex f being Function of R,S st
( f is RingHomomorphism & f is monomorphism );
end;

:: deftheorem Def3 defines -monomorphic RING_3:def 3 :
for R, S being Ring holds
( S is R -monomorphic iff ex f being Function of R,S st
( f is RingHomomorphism & f is monomorphism ) );

registration
let R be Ring;
existence
ex b1 being Ring st b1 is R -monomorphic
proof end;
end;

registration
let R be comRing;
existence
ex b1 being comRing st b1 is R -monomorphic
proof end;
existence
ex b1 being Ring st b1 is R -monomorphic
proof end;
end;

registration
let R be domRing;
existence
ex b1 being domRing st b1 is R -monomorphic
proof end;
existence
ex b1 being comRing st b1 is R -monomorphic
proof end;
existence
ex b1 being Ring st b1 is R -monomorphic
proof end;
end;

registration
let R be Field;
existence
ex b1 being Field st b1 is R -monomorphic
proof end;
existence
ex b1 being domRing st b1 is R -monomorphic
proof end;
existence
ex b1 being comRing st b1 is R -monomorphic
proof end;
existence
ex b1 being Ring st b1 is R -monomorphic
proof end;
end;

registration
let R be Ring;
let S be R -monomorphic Ring;
cluster Relation-like the carrier of R -defined the carrier of S -valued Function-like non empty V14( the carrier of R) quasi_total unity-preserving additive monomorphism multiplicative for Element of bool [: the carrier of R, the carrier of S:];
existence
ex b1 being Function of R,S st
( b1 is additive & b1 is multiplicative & b1 is unity-preserving & b1 is monomorphism )
proof end;
end;

definition end;

registration
let R be Ring;
let S be R -monomorphic Ring;
coherence
for b1 being S -monomorphic Ring holds b1 is R -monomorphic
proof end;
end;

registration
let R be Ring;
coherence
for b1 being R -monomorphic Ring holds b1 is R -homomorphic
proof end;
end;

registration
let R be Ring;
let S be R -monomorphic Ring;
let f be Monomorphism of R,S;
reduce (f ") " to f;
reducibility
(f ") " = f
by FUNCT_1:43;
end;

theorem Th68: :: RING_3:69
for R being Ring
for S being b1 -homomorphic Ring
for T being b2 -homomorphic Ring
for f being Homomorphism of R,S
for g being Homomorphism of S,T holds ker f c= ker (g * f)
proof end;

theorem Th69: :: RING_3:70
for R being Ring
for S being b1 -homomorphic Ring
for T being b2 -monomorphic Ring
for f being Homomorphism of R,S
for g being Monomorphism of S,T holds ker f = ker (g * f)
proof end;

theorem Th70: :: RING_3:71
for R being Ring
for S being Subring of R holds R is S -monomorphic
proof end;

theorem Th71: :: RING_3:72
for R, S being Ring holds
( S is b1 -monomorphic Ring iff S includes R )
proof end;

definition
let R, S be Ring;
attr S is R -isomorphic means :Def4: :: RING_3:def 4
ex f being Function of R,S st
( f is RingHomomorphism & f is isomorphism );
end;

:: deftheorem Def4 defines -isomorphic RING_3:def 4 :
for R, S being Ring holds
( S is R -isomorphic iff ex f being Function of R,S st
( f is RingHomomorphism & f is isomorphism ) );

registration
let R be Ring;
existence
ex b1 being Ring st b1 is R -isomorphic
proof end;
end;

registration
let R be comRing;
existence
ex b1 being comRing st b1 is R -isomorphic
proof end;
existence
ex b1 being Ring st b1 is R -isomorphic
proof end;
end;

registration
let R be domRing;
existence
ex b1 being domRing st b1 is R -isomorphic
proof end;
existence
ex b1 being comRing st b1 is R -isomorphic
proof end;
existence
ex b1 being Ring st b1 is R -isomorphic
proof end;
end;

registration
let R be Field;
existence
ex b1 being Field st b1 is R -isomorphic
proof end;
existence
ex b1 being domRing st b1 is R -isomorphic
proof end;
existence
ex b1 being comRing st b1 is R -isomorphic
proof end;
existence
ex b1 being Ring st b1 is R -isomorphic
proof end;
end;

registration
let R be Ring;
let S be R -isomorphic Ring;
cluster Relation-like the carrier of R -defined the carrier of S -valued Function-like non empty V14( the carrier of R) quasi_total unity-preserving additive isomorphism multiplicative for Element of bool [: the carrier of R, the carrier of S:];
existence
ex b1 being Function of R,S st
( b1 is additive & b1 is multiplicative & b1 is unity-preserving & b1 is isomorphism )
proof end;
end;

definition end;

definition
let R be Ring;
let S be R -isomorphic Ring;
let f be Isomorphism of R,S;
:: original: "
redefine func f " -> Function of S,R;
coherence
f " is Function of S,R
proof end;
end;

Lm7: for R being Ring
for S being b1 -isomorphic Ring
for f being Isomorphism of R,S holds
( f " is additive & f " is multiplicative & f " is unity-preserving & f " is isomorphism )

proof end;

registration
let R be Ring;
let S be R -isomorphic Ring;
cluster Relation-like the carrier of S -defined the carrier of R -valued Function-like non empty V14( the carrier of S) quasi_total unity-preserving additive isomorphism multiplicative for Element of bool [: the carrier of S, the carrier of R:];
existence
ex b1 being Function of S,R st
( b1 is additive & b1 is multiplicative & b1 is unity-preserving & b1 is isomorphism )
proof end;
end;

definition end;

registration
let R be Ring;
let S be R -isomorphic Ring;
coherence
for b1 being S -isomorphic Ring holds b1 is R -isomorphic
proof end;
end;

registration
let R be Ring;
coherence
for b1 being R -isomorphic Ring holds b1 is R -monomorphic
proof end;
end;

theorem Th72: :: RING_3:73
for R being Ring
for S being b1 -isomorphic Ring
for f being Isomorphism of R,S holds f " is Isomorphism of S,R by Lm7;

theorem :: RING_3:74
for R being Ring
for S being b1 -isomorphic Ring holds R is S -isomorphic
proof end;

registration
let R be comRing;
coherence
for b1 being R -isomorphic Ring holds b1 is commutative
proof end;
end;

registration
let R be domRing;
coherence
for b1 being R -isomorphic Ring holds
( not b1 is degenerated & b1 is domRing-like )
proof end;
end;

registration
let F be Field;
coherence
for b1 being F -isomorphic Ring holds b1 is almost_left_invertible
proof end;
end;

theorem :: RING_3:75
for E, F being Field holds
( E includes F iff ex K being strict Subfield of E st K,F are_isomorphic )
proof end;

definition
let R be Ring;
func Char R -> Nat means :Def5: :: RING_3:def 5
( ( it '*' (1. R) = 0. R & it <> 0 & ( for m being positive Nat st m < it holds
m '*' (1. R) <> 0. R ) ) or ( it = 0 & ( for m being positive Nat holds m '*' (1. R) <> 0. R ) ) );
existence
ex b1 being Nat st
( ( b1 '*' (1. R) = 0. R & b1 <> 0 & ( for m being positive Nat st m < b1 holds
m '*' (1. R) <> 0. R ) ) or ( b1 = 0 & ( for m being positive Nat holds m '*' (1. R) <> 0. R ) ) )
proof end;
uniqueness
for b1, b2 being Nat st ( ( b1 '*' (1. R) = 0. R & b1 <> 0 & ( for m being positive Nat st m < b1 holds
m '*' (1. R) <> 0. R ) ) or ( b1 = 0 & ( for m being positive Nat holds m '*' (1. R) <> 0. R ) ) ) & ( ( b2 '*' (1. R) = 0. R & b2 <> 0 & ( for m being positive Nat st m < b2 holds
m '*' (1. R) <> 0. R ) ) or ( b2 = 0 & ( for m being positive Nat holds m '*' (1. R) <> 0. R ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines Char RING_3:def 5 :
for R being Ring
for b2 being Nat holds
( b2 = Char R iff ( ( b2 '*' (1. R) = 0. R & b2 <> 0 & ( for m being positive Nat st m < b2 holds
m '*' (1. R) <> 0. R ) ) or ( b2 = 0 & ( for m being positive Nat holds m '*' (1. R) <> 0. R ) ) ) );

definition
let n be Nat;
let R be Ring;
attr R is n -characteristic means :Def6: :: RING_3:def 6
Char R = n;
end;

:: deftheorem Def6 defines -characteristic RING_3:def 6 :
for n being Nat
for R being Ring holds
( R is n -characteristic iff Char R = n );

Lm8: for i being Integer holds i '*' () = i
proof end;

theorem Th75: :: RING_3:76
proof end;

theorem Th76: :: RING_3:77
for n being positive Nat holds Char (Z/ n) = n
proof end;

registration
coherence by Th75;
end;

registration
let n be positive Nat;
coherence by Th76;
end;

registration
let n be Nat;
existence
ex b1 being comRing st b1 is n -characteristic
proof end;
end;

registration
let n be positive Nat;
let R be n -characteristic Ring;
coherence
Char R is positive
by Def6;
end;

definition
let R be Ring;
func CharSet R -> Subset of NAT equals :: RING_3:def 7
{ n where n is positive Nat : n '*' (1. R) = 0. R } ;
coherence
{ n where n is positive Nat : n '*' (1. R) = 0. R } is Subset of NAT
proof end;
end;

:: deftheorem defines CharSet RING_3:def 7 :
for R being Ring holds CharSet R = { n where n is positive Nat : n '*' (1. R) = 0. R } ;

registration
let n be positive Nat;
let R be n -characteristic Ring;
cluster CharSet R -> non empty ;
coherence
not CharSet R is empty
proof end;
end;

theorem Th77: :: RING_3:78
for R being Ring holds
( Char R = 0 iff CharSet R = {} )
proof end;

theorem Th78: :: RING_3:79
for n being positive Nat
for R being b1 -characteristic Ring holds Char R = min ()
proof end;

theorem Th79: :: RING_3:80
for R being Ring holds Char R = min* ()
proof end;

theorem :: RING_3:81
for p being Prime
for R being b1 -characteristic Ring
for n being positive Nat holds
( n is Element of CharSet R iff p divides n )
proof end;

definition
let R be Ring;
func canHom_Int R -> Function of INT.Ring,R means :Def8: :: RING_3:def 8
for x being Element of INT.Ring holds it . x = x '*' (1. R);
existence
ex b1 being Function of INT.Ring,R st
for x being Element of INT.Ring holds b1 . x = x '*' (1. R)
proof end;
uniqueness
for b1, b2 being Function of INT.Ring,R st ( for x being Element of INT.Ring holds b1 . x = x '*' (1. R) ) & ( for x being Element of INT.Ring holds b2 . x = x '*' (1. R) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines canHom_Int RING_3:def 8 :
for R being Ring
for b2 being Function of INT.Ring,R holds
( b2 = canHom_Int R iff for x being Element of INT.Ring holds b2 . x = x '*' (1. R) );

registration
let R be Ring;
coherence
proof end;
end;

registration
coherence
for b1 being Ring holds b1 is INT.Ring -homomorphic
proof end;
end;

theorem Th81: :: RING_3:82
for R being Ring
for n being non negative Element of INT.Ring holds
( Char R = n iff ker () = {n} -Ideal )
proof end;

theorem Th82: :: RING_3:83
for R being Ring holds
( Char R = 0 iff canHom_Int R is monomorphism )
proof end;

registration
let R be 0 -characteristic Ring;
coherence
proof end;
end;

registration
let R be 0 -characteristic Ring;
cluster Relation-like the carrier of INT.Ring -defined the carrier of R -valued Function-like non empty V14( the carrier of INT.Ring) quasi_total unity-preserving additive monomorphism multiplicative for Element of bool [: the carrier of INT.Ring, the carrier of R:];
existence
ex b1 being Function of INT.Ring,R st
( b1 is additive & b1 is multiplicative & b1 is unity-preserving & b1 is monomorphism )
proof end;
end;

theorem Th83: :: RING_3:84
for R being Ring
for f being Homomorphism of INT.Ring,R holds f = canHom_Int R
proof end;

theorem :: RING_3:85
for f being Homomorphism of INT.Ring,INT.Ring holds f = id INT.Ring
proof end;

theorem Th85: :: RING_3:86
for R being domRing holds
( Char R = 0 or Char R is prime )
proof end;

theorem :: RING_3:87
for R being Ring
for S being b1 -homomorphic Ring holds Char S divides Char R
proof end;

theorem Th87: :: RING_3:88
for R being Ring
for S being b1 -monomorphic Ring holds Char S = Char R
proof end;

theorem Th88: :: RING_3:89
for R being Ring
for S being Subring of R holds Char S = Char R
proof end;

registration
let n be Nat;
let R be n -characteristic Ring;
coherence
for b1 being Ring st b1 is R -monomorphic holds
b1 is n -characteristic
proof end;
cluster -> n -characteristic for Subring of R;
coherence
for b1 being Subring of R holds b1 is n -characteristic
proof end;
end;

Lm9: for n being Nat holds n '*' () = n
proof end;

registration
coherence
proof end;
end;

registration
coherence
proof end;
end;

registration
coherence
proof end;
end;

registration
existence
ex b1 being Field st b1 is 0 -characteristic
proof end;
end;

registration
let p be Prime;
existence
ex b1 being Field st b1 is p -characteristic
proof end;
end;

registration
let p be Prime;
let R be p -characteristic domRing;
cluster Char R -> prime ;
coherence
Char R is prime
by Th85;
end;

registration
let F be 0 -characteristic Field;
cluster -> 0 -characteristic for Subfield of F;
coherence
for b1 being Subfield of F holds b1 is 0 -characteristic
proof end;
end;

registration
let p be Prime;
let F be p -characteristic Field;
cluster -> p -characteristic for Subfield of F;
coherence
for b1 being Subfield of F holds b1 is p -characteristic
proof end;
end;

definition
let F be Field;
func carrier/\ F -> Subset of F equals :: RING_3:def 9
{ x where x is Element of F : for K being Subfield of F holds x in K } ;
coherence
{ x where x is Element of F : for K being Subfield of F holds x in K } is Subset of F
proof end;
end;

:: deftheorem defines carrier/\ RING_3:def 9 :
for F being Field holds carrier/\ F = { x where x is Element of F : for K being Subfield of F holds x in K } ;

definition
let F be Field;
func PrimeField F -> strict doubleLoopStr means :Def10: :: RING_3:def 10
( the carrier of it = carrier/\ F & the addF of it = the addF of F || () & the multF of it = the multF of F || () & the OneF of it = 1. F & the ZeroF of it = 0. F );
existence
ex b1 being strict doubleLoopStr st
( the carrier of b1 = carrier/\ F & the addF of b1 = the addF of F || () & the multF of b1 = the multF of F || () & the OneF of b1 = 1. F & the ZeroF of b1 = 0. F )
proof end;
uniqueness
for b1, b2 being strict doubleLoopStr st the carrier of b1 = carrier/\ F & the addF of b1 = the addF of F || () & the multF of b1 = the multF of F || () & the OneF of b1 = 1. F & the ZeroF of b1 = 0. F & the carrier of b2 = carrier/\ F & the addF of b2 = the addF of F || () & the multF of b2 = the multF of F || () & the OneF of b2 = 1. F & the ZeroF of b2 = 0. F holds
b1 = b2
;
end;

:: deftheorem Def10 defines PrimeField RING_3:def 10 :
for F being Field
for b2 being strict doubleLoopStr holds
( b2 = PrimeField F iff ( the carrier of b2 = carrier/\ F & the addF of b2 = the addF of F || () & the multF of b2 = the multF of F || () & the OneF of b2 = 1. F & the ZeroF of b2 = 0. F ) );

registration
let F be Field;
coherence
not PrimeField F is degenerated
proof end;
end;

Lm10: for F being Field
for x being Element of () holds x is Element of F

proof end;

Lm11: for F being Field
for a, b being Element of F
for x, y being Element of () st a = x & b = y holds
a + b = x + y

proof end;

Lm12: for F being Field
for a, b being Element of F
for x, y being Element of () st a = x & b = y holds
a * b = x * y

proof end;

registration
let F be Field;
coherence
proof end;
end;

registration
let F be Field;
coherence
proof end;
end;

registration
let F be Field;
coherence
proof end;
end;

definition
let F be Field;
:: original: PrimeField
redefine func PrimeField F -> strict Subfield of F;
coherence
PrimeField F is strict Subfield of F
proof end;
end;

Lm13: for F being Field
for K being Subfield of F holds carrier/\ F c= the carrier of K

proof end;

theorem Th89: :: RING_3:90
for F being Field
for E being strict Subfield of PrimeField F holds E = PrimeField F
proof end;

theorem Th90: :: RING_3:91
for F being Field
for E being Subfield of F holds PrimeField F is Subfield of E
proof end;

theorem Th91: :: RING_3:92
for F, K being Field holds
( K = PrimeField F iff ( K is strict Subfield of F & ( for E being strict Subfield of K holds E = K ) ) )
proof end;

theorem Th92: :: RING_3:93
for F, K being Field holds
( K = PrimeField F iff ( K is strict Subfield of F & ( for E being Subfield of F holds K is Subfield of E ) ) )
proof end;

theorem :: RING_3:94
for E being Field
for F being Subfield of E holds PrimeField F = PrimeField E
proof end;

theorem :: RING_3:95
for F being Field holds PrimeField () = PrimeField F by Th91;

registration
let F be Field;
coherence
proof end;
end;

theorem :: RING_3:96
for F being Field holds
( F is prime iff F = PrimeField F ) by EC_PF_1:def 2;

theorem Th96: :: RING_3:97
for F being 0 -characteristic Field
for i, j being non zero Integer st j divides i holds
(i div j) '*' (1. F) = (i '*' (1. F)) * ((j '*' (1. F)) ")
proof end;

definition
let x be Element of F_Rat;
:: original: denominator
redefine func denominator x -> positive Element of INT.Ring;
coherence by INT_1:def 2;
:: original: numerator
redefine func numerator x -> Element of INT.Ring;
coherence by INT_1:def 2;
end;

definition
let F be Field;
func canHom_Rat F -> Function of F_Rat,F means :Def11: :: RING_3:def 11
for x being Element of F_Rat holds it . x = (() . ()) / (() . ());
existence
ex b1 being Function of F_Rat,F st
for x being Element of F_Rat holds b1 . x = (() . ()) / (() . ())
proof end;
uniqueness
for b1, b2 being Function of F_Rat,F st ( for x being Element of F_Rat holds b1 . x = (() . ()) / (() . ()) ) & ( for x being Element of F_Rat holds b2 . x = (() . ()) / (() . ()) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines canHom_Rat RING_3:def 11 :
for F being Field
for b2 being Function of F_Rat,F holds
( b2 = canHom_Rat F iff for x being Element of F_Rat holds b2 . x = (() . ()) / (() . ()) );

registration
let F be Field;
coherence
proof end;
end;

registration
let F be 0 -characteristic Field;
coherence
proof end;
end;

registration
coherence
for b1 being 0 -characteristic Field holds b1 is F_Rat -monomorphic
proof end;
end;

theorem Th97: :: RING_3:98
for F being Field holds canHom_Int F = () | INT
proof end;

registration
existence
ex b1 being Field st
( b1 is 0 -characteristic & b1 is F_Rat -homomorphic )
;
end;

theorem Th98: :: RING_3:99
for F being F_Rat -homomorphic 0 -characteristic Field
for f being Homomorphism of F_Rat,F holds f = canHom_Rat F
proof end;

registration
coherence ;
end;

registration
let F be 0 -characteristic Field;
coherence ;
end;

theorem :: RING_3:100
for f being Homomorphism of F_Rat,F_Rat holds f = id F_Rat
proof end;

definition
let F be Field;
let S be F -homomorphic Field;
let f be Homomorphism of F,S;
:: original: Image
redefine func Image f -> strict Subfield of S;
coherence
Image f is strict Subfield of S
proof end;
end;

registration
let F be 0 -characteristic Field;
coherence
canHom_Rat () is onto
proof end;
end;

theorem Th100: :: RING_3:101
for F being 0 -characteristic Field holds F_Rat , PrimeField F are_isomorphic
proof end;

theorem :: RING_3:102

theorem :: RING_3:103
for F being 0 -characteristic Field holds F includes F_Rat by Th71;

theorem :: RING_3:104
for F being 0 -characteristic Field
for E being Field st F includes E holds
E includes F_Rat
proof end;

theorem Th104: :: RING_3:105
for p being Prime
for R being b1 -characteristic Ring
for i being Integer holds i '*' (1. R) = (i mod p) '*' (1. R)
proof end;

definition
let p be Prime;
let F be Field;
func canHom_Z/ (p,F) -> Function of (Z/ p),F equals :: RING_3:def 12
() | the carrier of (Z/ p);
coherence
() | the carrier of (Z/ p) is Function of (Z/ p),F
proof end;
end;

:: deftheorem defines canHom_Z/ RING_3:def 12 :
for p being Prime
for F being Field holds canHom_Z/ (p,F) = () | the carrier of (Z/ p);

Lm14: for p being Prime
for F being Field
for x being Element of (Z/ p)
for y being Element of INT.Ring st x = y holds
(canHom_Z/ (p,F)) . x = y '*' (1. F)

proof end;

registration
let p be Prime;
let F be Field;
cluster canHom_Z/ (p,F) -> unity-preserving ;
coherence
canHom_Z/ (p,F) is unity-preserving
proof end;
end;

registration
let p be Prime;
let F be p -characteristic Field;
coherence
( canHom_Z/ (p,F) is additive & canHom_Z/ (p,F) is multiplicative )
proof end;
end;

registration
let p be Prime;
coherence
for b1 being p -characteristic Field holds b1 is Z/ p -monomorphic
proof end;
end;

registration
let p be Prime;
existence
ex b1 being Field st
( b1 is p -characteristic & b1 is Z/ p -homomorphic )
;
coherence
Z/ p is Z/ p -homomorphic
;
end;

theorem Th105: :: RING_3:106
for p being Prime
for F being Z/ b1 -homomorphic b1 -characteristic Field
for f being Homomorphism of (Z/ p),F holds f = canHom_Z/ (p,F)
proof end;

theorem :: RING_3:107
for p being Prime
for f being Homomorphism of (Z/ p),(Z/ p) holds f = id (Z/ p)
proof end;

registration
let p be Prime;
let F be p -characteristic Field;
coherence ;
end;

registration
let p be Prime;
let F be p -characteristic Field;
cluster canHom_Z/ (p,()) -> onto ;
coherence
canHom_Z/ (p,()) is onto
proof end;
end;

theorem Th107: :: RING_3:108
for p being Prime
for F being b1 -characteristic Field holds Z/ p, PrimeField F are_isomorphic
proof end;

theorem :: RING_3:109
for p being Prime
for F being strict Subfield of Z/ p holds F = Z/ p by EC_PF_1:def 2;

theorem :: RING_3:110
for p being Prime holds PrimeField (Z/ p) = Z/ p by EC_PF_1:def 2;

theorem :: RING_3:111
for p being Prime
for F being b1 -characteristic Field holds F includes Z/ p by Th71;

theorem :: RING_3:112
for p being Prime
for F being b1 -characteristic Field
for E being Field st F includes E holds
E includes Z/ p
proof end;

registration
let p be Prime;
cluster Z/ p -> prime ;
coherence
Z/ p is prime
;
end;

theorem :: RING_3:113
for F being Field holds
( Char F = 0 iff PrimeField F, F_Rat are_isomorphic )
proof end;

theorem :: RING_3:114
for p being Prime
for F being Field holds
( Char F = p iff PrimeField F, Z/ p are_isomorphic )
proof end;

theorem :: RING_3:115
for F being strict Field holds
( F is prime iff ( F, F_Rat are_isomorphic or ex p being Prime st F, Z/ p are_isomorphic ) )
proof end;