:: The First Isomorphism Theorem and Other Properties of Rings
:: by Artur Korni{\l}owicz and Christoph Schwarzweller
::
:: Copyright (c) 2014-2021 Association of Mizar Users

definition
let R be non empty set ;
let f be non empty FinSequence of R;
let x be Element of dom f;
:: original: .
redefine func f . x -> Element of R;
coherence
f . x is Element of R
proof end;
end;

registration
let X be set ;
let F1, F2 be X -valued FinSequence;
cluster F1 ^ F2 -> X -valued ;
coherence
F1 ^ F2 is X -valued
proof end;
end;

theorem prod4: :: RING_2:1
for R being non empty right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for F being FinSequence of R st ex i being Nat st
( i in dom F & F . i = 0. R ) holds
Product F = 0. R
proof end;

theorem prod5: :: RING_2:2
for R being non degenerated right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for F being FinSequence of R holds
( Product F = 0. R iff ex i being Nat st
( i in dom F & F . i = 0. R ) )
proof end;

definition
let X be set ;
mode Chain of X is sequence of X;
end;

definition
let X be non empty set ;
let C be Chain of X;
attr C is ascending means :asc: :: RING_2:def 1
for i being Nat holds C . i c= C . (i + 1);
attr C is stagnating means :: RING_2:def 2
ex i being Nat st
for j being Nat st j >= i holds
C . j = C . i;
end;

:: deftheorem asc defines ascending RING_2:def 1 :
for X being non empty set
for C being Chain of X holds
( C is ascending iff for i being Nat holds C . i c= C . (i + 1) );

:: deftheorem defines stagnating RING_2:def 2 :
for X being non empty set
for C being Chain of X holds
( C is stagnating iff ex i being Nat st
for j being Nat st j >= i holds
C . j = C . i );

registration
let X be non empty set ;
let x be Element of X;
cluster NAT --> x -> ascending stagnating for Chain of X;
coherence
for b1 being Chain of X st b1 = NAT --> x holds
( b1 is ascending & b1 is stagnating )
proof end;
end;

registration
let X be non empty set ;
existence
ex b1 being Chain of X st
( b1 is ascending & b1 is stagnating )
proof end;
end;

ch1: for X being non empty set
for C being ascending Chain of X
for x being object
for i, j being Nat st i <= j & x in C . i holds
x in C . j

proof end;

theorem :: RING_2:3
for X being non empty set
for C being ascending Chain of X
for i, j being Nat st i <= j holds
C . i c= C . j by ch1;

definition
let R be Ring;
func Ideals R -> Subset-Family of the carrier of R equals :: RING_2:def 3
{ I where I is Ideal of R : verum } ;
coherence
{ I where I is Ideal of R : verum } is Subset-Family of the carrier of R
proof end;
end;

:: deftheorem defines Ideals RING_2:def 3 :
for R being Ring holds Ideals R = { I where I is Ideal of R : verum } ;

registration
let R be Ring;
cluster Ideals R -> non empty ;
coherence
not Ideals R is empty
proof end;
end;

theorem id2: :: RING_2:4
for R being comRing
for I being Ideal of R
for a being Element of R st a in I holds
{a} -Ideal c= I
proof end;

theorem id1: :: RING_2:5
for R being Ring
for C being ascending Chain of () holds union { (C . i) where i is Nat : verum } is Ideal of R
proof end;

registration
let R be non empty doubleLoopStr ;
let S be non empty right_zeroed doubleLoopStr ;
cluster R --> (0. S) -> additive ;
coherence
R --> (0. S) is additive
proof end;
end;

registration
let R be non empty doubleLoopStr ;
let S be non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr ;
cluster R --> (0. S) -> multiplicative ;
coherence
R --> (0. S) is multiplicative
proof end;
end;

registration
let R be non empty well-unital doubleLoopStr ;
let S be non degenerated well-unital doubleLoopStr ;
cluster R --> (0. S) -> non unity-preserving ;
coherence
not R --> (0. S) is unity-preserving
by FUNCOP_1:7;
end;

registration
let R be non empty doubleLoopStr ;
coherence
( id R is additive & id R is multiplicative & id R is unity-preserving )
;
end;

registration
let R be non empty doubleLoopStr ;
coherence
( id R is RingMonomorphism & id R is RingEpimorphism )
;
end;

registration
let R be non empty doubleLoopStr ;
let S be non empty right_zeroed doubleLoopStr ;
cluster Relation-like the carrier of R -defined the carrier of S -valued Function-like non empty total quasi_total additive for Element of bool [: the carrier of R, the carrier of S:];
existence
ex b1 being Function of R,S st b1 is additive
proof end;
end;

registration
let R be non empty doubleLoopStr ;
let S be non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr ;
cluster Relation-like the carrier of R -defined the carrier of S -valued Function-like non empty total quasi_total multiplicative for Element of bool [: the carrier of R, the carrier of S:];
existence
ex b1 being Function of R,S st b1 is multiplicative
proof end;
end;

registration
let R, S be non empty well-unital doubleLoopStr ;
cluster Relation-like the carrier of R -defined the carrier of S -valued Function-like non empty total quasi_total unity-preserving for Element of bool [: the carrier of R, the carrier of S:];
existence
ex b1 being Function of R,S st b1 is unity-preserving
proof end;
end;

registration
let R be non empty doubleLoopStr ;
let S be non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr ;
cluster Relation-like the carrier of R -defined the carrier of S -valued Function-like non empty total quasi_total additive 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 )
proof end;
end;

definition
let R, S be Ring;
attr S is R -homomorphic means :defhom: :: RING_2:def 4
ex f being Function of R,S st f is RingHomomorphism ;
end;

:: deftheorem defhom defines -homomorphic RING_2:def 4 :
for R, S being Ring holds
( S is R -homomorphic iff ex f being Function of R,S st f is RingHomomorphism );

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

registration
let R be comRing;
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 Field 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 Ring;
let S be R -homomorphic Ring;
cluster Relation-like the carrier of R -defined the carrier of S -valued Function-like non empty total quasi_total additive unity-preserving 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 )
proof end;
end;

definition end;

registration
let R, S, T be Ring;
let f be unity-preserving Function of R,S;
let g be unity-preserving Function of S,T;
cluster f * g -> unity-preserving for Function of R,T;
coherence
for b1 being Function of R,T st b1 = g * f holds
b1 is unity-preserving
proof end;
end;

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

notation
let R, S be non empty doubleLoopStr ;
synonym R,S are_isomorphic for R is_ringisomorph_to S;
end;

theorem hom1: :: RING_2:6
for R being non empty right_complementable add-associative right_zeroed doubleLoopStr
for S being non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr
for f being additive Function of R,S holds f . (0. R) = 0. S
proof end;

theorem hom4a: :: RING_2:7
for R being non empty right_complementable add-associative right_zeroed doubleLoopStr
for S being non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr
for f being additive Function of R,S
for x being Element of R holds f . (- x) = - (f . x)
proof end;

theorem hom4: :: RING_2:8
for R being non empty right_complementable add-associative right_zeroed doubleLoopStr
for S being non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr
for f being additive Function of R,S
for x, y being Element of R holds f . (x - y) = (f . x) - (f . y)
proof end;

theorem hom2: :: RING_2:9
for R being non empty right_unital doubleLoopStr
for S being non empty right_complementable right-distributive right_unital Abelian add-associative right_zeroed domRing-like doubleLoopStr
for f being multiplicative Function of R,S holds
( f . (1. R) = 0. S or f . (1. R) = 1. S )
proof end;

hom3: for E, F being Field
for f being additive multiplicative Function of E,F holds
( ( f . (1. E) = 0. F & f = E --> (0. F) ) or ( f . (1. E) = 1. F & f is monomorphism ) )

proof end;

theorem :: RING_2:10
for E, F being Field
for f being additive multiplicative Function of E,F holds
( f . (1. E) = 0. F iff f = E --> (0. F) )
proof end;

theorem hom3a: :: RING_2:11
for E, F being Field
for f being additive multiplicative Function of E,F holds
( f . (1. E) = 1. F iff f is monomorphism )
proof end;

registration
let E, F be Field;
cluster Function-like quasi_total additive unity-preserving multiplicative -> monomorphism for Element of bool [: the carrier of E, the carrier of F:];
coherence
for b1 being Function of E,F st b1 is additive & b1 is multiplicative & b1 is unity-preserving holds
b1 is monomorphism
by hom3a;
end;

definition
let R be Ring;
let I be Ideal of R;
func canHom I -> Function of R,(R / I) means :defhomI: :: RING_2:def 5
for a being Element of R holds it . a = Class ((EqRel (R,I)),a);
existence
ex b1 being Function of R,(R / I) st
for a being Element of R holds b1 . a = Class ((EqRel (R,I)),a)
proof end;
uniqueness
for b1, b2 being Function of R,(R / I) st ( for a being Element of R holds b1 . a = Class ((EqRel (R,I)),a) ) & ( for a being Element of R holds b2 . a = Class ((EqRel (R,I)),a) ) holds
b1 = b2
proof end;
end;

:: deftheorem defhomI defines canHom RING_2:def 5 :
for R being Ring
for I being Ideal of R
for b3 being Function of R,(R / I) holds
( b3 = canHom I iff for a being Element of R holds b3 . a = Class ((EqRel (R,I)),a) );

registration
let R be Ring;
let I be Ideal of R;
coherence
proof end;
end;

registration
let R be Ring;
let I be Ideal of R;
coherence
proof end;
end;

registration
let R be Ring;
let I be Ideal of R;
cluster QuotientRing (R,I) -> R -homomorphic ;
coherence
R / I is R -homomorphic
proof end;
end;

registration
let R be non empty right_complementable add-associative right_zeroed doubleLoopStr ;
let S be non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr ;
let f be additive Function of R,S;
cluster ker f -> non empty ;
coherence
not ker f is empty
proof end;
end;

ker1: for R, S being non empty doubleLoopStr
for f being Function of R,S
for x being Element of R st x in ker f holds
f . x = 0. S

proof end;

registration
let R be non empty doubleLoopStr ;
let S be non empty right_complementable add-associative right_zeroed doubleLoopStr ;
let f be additive Function of R,S;
coherence
proof end;
end;

registration
let R be non empty doubleLoopStr ;
let S be non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr ;
let f be multiplicative Function of R,S;
coherence
proof end;
end;

registration
let R be non empty doubleLoopStr ;
let S be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ;
let f be multiplicative Function of R,S;
coherence
proof end;
end;

registration
let R be non empty well-unital doubleLoopStr ;
let S be non degenerated well-unital doubleLoopStr ;
let f be unity-preserving Function of R,S;
cluster ker f -> proper ;
coherence
ker f is proper
proof end;
end;

theorem ker0: :: RING_2:12
for R being Ring
for S being b1 -homomorphic Ring
for f being Homomorphism of R,S holds
( f is monomorphism iff ker f = {(0. R)} )
proof end;

theorem kercanhomI: :: RING_2:13
for R being Ring
for I being Ideal of R holds ker () = I
proof end;

theorem :: RING_2:14
for R being Ring
for I being Subset of R holds
( I is Ideal of R iff ex S being b1 -homomorphic Ring ex f being Homomorphism of R,S st ker f = I )
proof end;

T0: for R being Ring
for S being b1 -homomorphic Ring
for f being Homomorphism of R,S holds 0. S in rng f

proof end;

T1: for R being Ring
for S being b1 -homomorphic Ring
for f being Homomorphism of R,S holds 1. S in rng f

proof end;

T3: for R being Ring
for S being b1 -homomorphic Ring
for f being Homomorphism of R,S holds rng f is Preserv of the addF of S

proof end;

T4: for R being Ring
for S being b1 -homomorphic Ring
for f being Homomorphism of R,S holds rng f is Preserv of the multF of S

proof end;

definition
let R be Ring;
let S be R -homomorphic Ring;
let f be Homomorphism of R,S;
func Image f -> strict doubleLoopStr means :defim: :: RING_2:def 6
( the carrier of it = rng f & the addF of it = the addF of S || (rng f) & the multF of it = the multF of S || (rng f) & the OneF of it = 1. S & the ZeroF of it = 0. S );
existence
ex b1 being strict doubleLoopStr st
( the carrier of b1 = rng f & the addF of b1 = the addF of S || (rng f) & the multF of b1 = the multF of S || (rng f) & the OneF of b1 = 1. S & the ZeroF of b1 = 0. S )
proof end;
uniqueness
for b1, b2 being strict doubleLoopStr st the carrier of b1 = rng f & the addF of b1 = the addF of S || (rng f) & the multF of b1 = the multF of S || (rng f) & the OneF of b1 = 1. S & the ZeroF of b1 = 0. S & the carrier of b2 = rng f & the addF of b2 = the addF of S || (rng f) & the multF of b2 = the multF of S || (rng f) & the OneF of b2 = 1. S & the ZeroF of b2 = 0. S holds
b1 = b2
;
end;

:: deftheorem defim defines Image RING_2:def 6 :
for R being Ring
for S being b1 -homomorphic Ring
for f being Homomorphism of R,S
for b4 being strict doubleLoopStr holds
( b4 = Image f iff ( the carrier of b4 = rng f & the addF of b4 = the addF of S || (rng f) & the multF of b4 = the multF of S || (rng f) & the OneF of b4 = 1. S & the ZeroF of b4 = 0. S ) );

T5: for R being Ring
for S being b1 -homomorphic Ring
for f being Homomorphism of R,S
for a, b being Element of ()
for x, y being Element of S st a = x & b = y holds
( a + b = x + y & a * b = x * y )

proof end;

T6: for R being Ring
for S being b1 -homomorphic Ring
for f being Homomorphism of R,S
for a being Element of () ex x being Element of R st f . x = a

proof end;

registration
let R be Ring;
let S be R -homomorphic Ring;
let f be Homomorphism of R,S;
cluster Image f -> non empty strict ;
coherence
not Image f is empty
proof end;
end;

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

registration
let R be Ring;
let S be R -homomorphic Ring;
let f be Homomorphism of R,S;
coherence
( Image f is associative & Image f is well-unital & Image f is distributive )
proof end;
end;

registration
let R be comRing;
let S be R -homomorphic comRing;
let f be Homomorphism of R,S;
coherence
proof end;
end;

definition
let R be Ring;
let S be R -homomorphic Ring;
let f be Homomorphism of R,S;
:: original: Image
redefine func Image f -> strict Subring of S;
coherence
Image f is strict Subring of S
proof end;
end;

definition
let R be Ring;
let S be R -homomorphic Ring;
let f be Homomorphism of R,S;
func canHom f -> Function of (R / (ker f)),() means :ch: :: RING_2:def 7
for a being Element of R holds it . (Class ((EqRel (R,(ker f))),a)) = f . a;
existence
ex b1 being Function of (R / (ker f)),() st
for a being Element of R holds b1 . (Class ((EqRel (R,(ker f))),a)) = f . a
proof end;
uniqueness
for b1, b2 being Function of (R / (ker f)),() st ( for a being Element of R holds b1 . (Class ((EqRel (R,(ker f))),a)) = f . a ) & ( for a being Element of R holds b2 . (Class ((EqRel (R,(ker f))),a)) = f . a ) holds
b1 = b2
proof end;
end;

:: deftheorem ch defines canHom RING_2:def 7 :
for R being Ring
for S being b1 -homomorphic Ring
for f being Homomorphism of R,S
for b4 being Function of (R / (ker f)),() holds
( b4 = canHom f iff for a being Element of R holds b4 . (Class ((EqRel (R,(ker f))),a)) = f . a );

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

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

theorem :: RING_2:15
for R being Ring
for S being b1 -homomorphic Ring
for f being Homomorphism of R,S holds R / (ker f), Image f are_isomorphic
proof end;

theorem :: RING_2:16
for R being Ring
for S being b1 -homomorphic Ring
for f being Homomorphism of R,S st f is onto holds
R / (ker f),S are_isomorphic
proof end;

theorem :: RING_2:17
for R being Ring holds R / {(0. R)},R are_isomorphic
proof end;

registration
let R be Ring;
cluster QuotientRing (R,([#] R)) -> trivial ;
coherence
R / ([#] R) is trivial
proof end;
end;

registration
let L be non empty right_unital multLoopStr ;
cluster unital for Element of the carrier of L;
existence
ex b1 being Element of L st b1 is unital
proof end;
end;

definition
let L be non empty right_unital multLoopStr ;
mode Unit of L is unital Element of L;
end;

registration
let L be non degenerated right_complementable left-distributive add-associative right_zeroed doubleLoopStr ;
existence
not for b1 being Element of L holds b1 is unital
proof end;
end;

definition end;

registration
let L be non degenerated right_complementable left-distributive add-associative right_zeroed doubleLoopStr ;
cluster 0. L -> non unital ;
coherence
not 0. L is unital
proof end;
end;

registration
let L be non empty right_unital multLoopStr ;
cluster 1. L -> unital ;
coherence
1. L is unital
proof end;
end;

registration
let L be non degenerated right_complementable left-distributive right_unital add-associative right_zeroed doubleLoopStr ;
cluster unital -> non zero for Element of the carrier of L;
coherence
for b1 being Unit of L holds not b1 is zero
;
end;

registration
let F be Field;
cluster non zero -> non zero unital for Element of the carrier of F;
coherence
for b1 being non zero Element of F holds b1 is unital
proof end;
end;

registration
let R be domRing;
let u, v be unital Element of R;
cluster u * v -> unital ;
coherence
u * v is unital
proof end;
end;

theorem div0: :: RING_2:18
for R being comRing
for a, b being Element of R holds
( a divides b iff b in {a} -Ideal )
proof end;

theorem div1: :: RING_2:19
for R being comRing
for a, b being Element of R holds
( a divides b iff {b} -Ideal c= {a} -Ideal )
proof end;

theorem div2: :: RING_2:20
for R being comRing
for a being Element of R holds
( a is Unit of R iff {a} -Ideal = [#] R )
proof end;

theorem div3: :: RING_2:21
for R being comRing
for a, b being Element of R holds
( a is_associated_to b iff {a} -Ideal = {b} -Ideal ) by div1;

definition
let R be non empty right_unital doubleLoopStr ;
let x be Element of R;
attr x is prime means :defprim: :: RING_2:def 8
( x <> 0. R & x is not Unit of R & ( for a, b being Element of R holds
( not x divides a * b or x divides a or x divides b ) ) );
attr x is irreducible means :: RING_2:def 9
( x <> 0. R & x is not Unit of R & ( for a being Element of R holds
( not a divides x or a is Unit of R or a is_associated_to x ) ) );
end;

:: deftheorem defprim defines prime RING_2:def 8 :
for R being non empty right_unital doubleLoopStr
for x being Element of R holds
( x is prime iff ( x <> 0. R & x is not Unit of R & ( for a, b being Element of R holds
( not x divides a * b or x divides a or x divides b ) ) ) );

:: deftheorem defines irreducible RING_2:def 9 :
for R being non empty right_unital doubleLoopStr
for x being Element of R holds
( x is irreducible iff ( x <> 0. R & x is not Unit of R & ( for a being Element of R holds
( not a divides x or a is Unit of R or a is_associated_to x ) ) ) );

notation
let R be non empty right_unital doubleLoopStr ;
let x be Element of R;
antonym reducible x for irreducible ;
end;

registration
let R be non empty right_unital doubleLoopStr ;
cluster non prime for Element of the carrier of R;
existence
not for b1 being Element of R holds b1 is prime
proof end;
end;

lemintr: for x, y being Integer
for a, b being Element of INT.Ring st x <> 0 & x = a & y = b holds
( x divides y iff a divides b )

proof end;

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

registration
let R be non empty right_unital doubleLoopStr ;
cluster prime -> non zero non unital for Element of the carrier of R;
coherence
for b1 being Element of R st b1 is prime holds
( not b1 is zero & not b1 is unital )
;
cluster irreducible -> non zero non unital for Element of the carrier of R;
coherence
for b1 being Element of R st b1 is irreducible holds
( not b1 is zero & not b1 is unital )
;
end;

registration
let R be domRing;
cluster prime -> irreducible for Element of the carrier of R;
coherence
for b1 being Element of R st b1 is prime holds
b1 is irreducible
proof end;
end;

registration
let F be Field;
cluster -> reducible for Element of the carrier of F;
coherence
for b1 being Element of F holds b1 is reducible
;
end;

definition
let R be non empty right_unital doubleLoopStr ;
func IRR R -> Subset of R equals :: RING_2:def 10
{ x where x is Element of R : x is irreducible } ;
coherence
{ x where x is Element of R : x is irreducible } is Subset of R
proof end;
end;

:: deftheorem defines IRR RING_2:def 10 :
for R being non empty right_unital doubleLoopStr holds IRR R = { x where x is Element of R : x is irreducible } ;

registration
let F be Field;
cluster IRR F -> empty ;
coherence
IRR F is empty
proof end;
end;

theorem ass0: :: RING_2:22
for R being domRing
for c being non zero Element of R
for b, a, d being Element of R st a * b is_associated_to c * d & a is_associated_to c holds
b is_associated_to d
proof end;

theorem ass1: :: RING_2:23
for R being domRing
for a, b being Element of R st a is irreducible & b is_associated_to a holds
b is irreducible
proof end;

theorem thpr: :: RING_2:24
for R being non degenerated comRing
for a being non zero Element of R holds
( a is prime iff {a} -Ideal is prime )
proof end;

theorem maxirr: :: RING_2:25
for R being non degenerated comRing
for a being non zero Element of R st {a} -Ideal is maximal holds
a is irreducible
proof end;

registration
coherence
for b1 being Field holds b1 is PID
proof end;
end;

registration
cluster non empty PID for doubleLoopStr ;
existence
ex b1 being non empty doubleLoopStr st b1 is PID
proof end;
end;

definition end;

theorem maxirr2: :: RING_2:26
for R being PIDomain
for a being non zero Element of R holds
( {a} -Ideal is maximal iff a is irreducible )
proof end;

registration
let R be PIDomain;
cluster irreducible -> prime for Element of the carrier of R;
coherence
for b1 being Element of R st b1 is irreducible holds
b1 is prime
proof end;
end;

registration
coherence
for b1 being comRing st b1 is Euclidian holds
b1 is PID
by IDEAL_1:94;
end;

registration
let R be PIDomain;
coherence
for b1 being Chain of () st b1 is ascending holds
b1 is stagnating
proof end;
end;

definition
let R be non empty right_unital doubleLoopStr ;
let x be Element of R;
let F be non empty FinSequence of R;
pred F is_a_factorization_of x means :: RING_2:def 11
( x = Product F & ( for i being Element of dom F holds F . i is irreducible ) );
end;

:: deftheorem defines is_a_factorization_of RING_2:def 11 :
for R being non empty right_unital doubleLoopStr
for x being Element of R
for F being non empty FinSequence of R holds
( F is_a_factorization_of x iff ( x = Product F & ( for i being Element of dom F holds F . i is irreducible ) ) );

definition
let R be non empty right_unital doubleLoopStr ;
let x be Element of R;
attr x is factorizable means :: RING_2:def 12
ex F being non empty FinSequence of R st F is_a_factorization_of x;
end;

:: deftheorem defines factorizable RING_2:def 12 :
for R being non empty right_unital doubleLoopStr
for x being Element of R holds
( x is factorizable iff ex F being non empty FinSequence of R st F is_a_factorization_of x );

definition
let R be non empty right_unital doubleLoopStr ;
let x be Element of R;
assume AS: x is factorizable ;
mode Factorization of x -> non empty FinSequence of R means :ddf: :: RING_2:def 13
it is_a_factorization_of x;
existence
ex b1 being non empty FinSequence of R st b1 is_a_factorization_of x
by AS;
end;

:: deftheorem ddf defines Factorization RING_2:def 13 :
for R being non empty right_unital doubleLoopStr
for x being Element of R st x is factorizable holds
for b3 being non empty FinSequence of R holds
( b3 is Factorization of x iff b3 is_a_factorization_of x );

definition
let R be non empty right_unital doubleLoopStr ;
let x be Element of R;
attr x is uniquely_factorizable means :: RING_2:def 14
( x is factorizable & ( for F, G being Factorization of x ex B being Function of (dom F),(dom G) st
( B is bijective & ( for i being Element of dom F holds G . (B . i) is_associated_to F . i ) ) ) );
end;

:: deftheorem defines uniquely_factorizable RING_2:def 14 :
for R being non empty right_unital doubleLoopStr
for x being Element of R holds
( x is uniquely_factorizable iff ( x is factorizable & ( for F, G being Factorization of x ex B being Function of (dom F),(dom G) st
( B is bijective & ( for i being Element of dom F holds G . (B . i) is_associated_to F . i ) ) ) ) );

registration
let R be non empty right_unital doubleLoopStr ;
cluster uniquely_factorizable -> factorizable for Element of the carrier of R;
coherence
for b1 being Element of R st b1 is uniquely_factorizable holds
b1 is factorizable
;
end;

registration
let R be domRing;
cluster factorizable -> non zero non unital for Element of the carrier of R;
coherence
for b1 being Element of R st b1 is factorizable holds
( not b1 is zero & not b1 is unital )
proof end;
end;

fact1: for R being non empty right_unital doubleLoopStr
for a being Element of R holds
( a is irreducible iff <*a*> is_a_factorization_of a )

proof end;

registration
let R be non empty right_unital doubleLoopStr ;
cluster irreducible -> factorizable for Element of the carrier of R;
coherence
for b1 being Element of R st b1 is irreducible holds
b1 is factorizable
proof end;
end;

theorem :: RING_2:27
for R being non empty right_unital doubleLoopStr
for a being Element of R holds
( a is irreducible iff <*a*> is_a_factorization_of a ) by fact1;

theorem fact2: :: RING_2:28
for R being non empty well-unital associative doubleLoopStr
for a, b being Element of R
for F, G being non empty FinSequence of R st F is_a_factorization_of a & G is_a_factorization_of b holds
F ^ G is_a_factorization_of a * b
proof end;

lemfactunique1: for R being domRing
for a, b, x being Element of R
for F being non empty FinSequence of R st x is prime & x divides a & a is_associated_to b & F is_a_factorization_of b holds
ex i being Element of dom F st F . i is_associated_to x

proof end;

lemfactunique: for R being PIDomain
for x, y being Element of R
for F, G being non empty FinSequence of R st F is_a_factorization_of x & G is_a_factorization_of y & x is_associated_to y holds
ex p being Function of (dom F),(dom G) st
( p is bijective & ( for i being Element of dom F holds G . (p . i) is_associated_to F . i ) )

proof end;

registration
let R be PIDomain;
cluster factorizable -> uniquely_factorizable for Element of the carrier of R;
coherence
for b1 being Element of R st b1 is factorizable holds
b1 is uniquely_factorizable
proof end;
end;

definition
let R be non degenerated Ring;
attr R is factorial means :df: :: RING_2:def 15
for a being non zero Element of R st a is NonUnit of R holds
a is uniquely_factorizable ;
end;

:: deftheorem df defines factorial RING_2:def 15 :
for R being non degenerated Ring holds
( R is factorial iff for a being non zero Element of R st a is NonUnit of R holds
a is uniquely_factorizable );

registration
existence
ex b1 being non degenerated Ring st b1 is factorial
proof end;
end;

registration
let R be non degenerated factorial Ring;
cluster non zero non unital -> factorizable for Element of the carrier of R;
coherence
for b1 being Element of R st not b1 is zero & not b1 is unital holds
b1 is factorizable
proof end;
end;

definition end;

registration
coherence
for b1 being domRing st b1 is PID holds
b1 is factorial
proof end;
end;

definition
let L be Field;
let p be Polynomial of L;
func deg* p -> Nat equals :S: :: RING_2:def 16
deg p if p <> 0_. L
otherwise 0 ;
coherence
( ( p <> 0_. L implies deg p is Nat ) & ( not p <> 0_. L implies 0 is Nat ) )
proof end;
consistency
for b1 being Nat holds verum
;
end;

:: deftheorem S defines deg* RING_2:def 16 :
for L being Field
for p being Polynomial of L holds
( ( p <> 0_. L implies deg* p = deg p ) & ( not p <> 0_. L implies deg* p = 0 ) );

definition
let L be Field;
func deg* L -> Function of (),NAT means :T: :: RING_2:def 17
for p being Polynomial of L holds it . p = deg* p;
existence
ex b1 being Function of (),NAT st
for p being Polynomial of L holds b1 . p = deg* p
proof end;
uniqueness
for b1, b2 being Function of (),NAT st ( for p being Polynomial of L holds b1 . p = deg* p ) & ( for p being Polynomial of L holds b2 . p = deg* p ) holds
b1 = b2
proof end;
end;

:: deftheorem T defines deg* RING_2:def 17 :
for L being Field
for b2 being Function of (),NAT holds
( b2 = deg* L iff for p being Polynomial of L holds b2 . p = deg* p );

theorem degA: :: RING_2:29
for L being Field
for p being Polynomial of L
for q being non zero Polynomial of L holds deg (p mod q) < deg q
proof end;

theorem thEucl1: :: RING_2:30
for L being Field
for p being Element of ()
for q being non zero Element of () ex u, r being Element of () st
( p = (u * q) + r & ( r = 0. () or (deg* L) . r < (deg* L) . q ) )
proof end;

thEucl2: for L being Field ex f being Function of (),NAT st
for p, q being Element of () st q <> 0. () holds
ex u, r being Element of () st
( p = (u * q) + r & ( r = 0. () or f . r < f . q ) )

proof end;

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

definition
let L be Field;
:: original: deg*
redefine func deg* L -> DegreeFunction of Polynom-Ring L;
coherence
proof end;
end;