begin
theorem Th1:
:: deftheorem Def1 defines divides GCD_1:def 1 :
for R being non empty multMagma
for x, y being Element of R holds
( x divides y iff ex z being Element of R st y = x * z );
:: deftheorem Def2 defines unital GCD_1:def 2 :
for R being non empty multLoopStr
for x being Element of R holds
( x is unital iff x divides 1. R );
:: deftheorem Def3 defines is_associated_to GCD_1:def 3 :
for R being non empty multLoopStr
for x, y being Element of R holds
( x is_associated_to y iff ( x divides y & y divides x ) );
:: deftheorem Def4 defines / GCD_1:def 4 :
for R being commutative domRing-like Ring
for x, y being Element of R st y divides x & y <> 0. R holds
for b4 being Element of R holds
( b4 = x / y iff b4 * y = x );
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem
theorem Th14:
theorem Th15:
theorem
theorem Th17:
theorem Th18:
theorem Th19:
begin
:: deftheorem Def5 defines Class GCD_1:def 5 :
for R being non empty multLoopStr
for a being Element of R
for b3 being Subset of R holds
( b3 = Class a iff for b being Element of R holds
( b in b3 iff b is_associated_to a ) );
theorem Th20:
:: deftheorem Def6 defines Classes GCD_1:def 6 :
for R being non empty multLoopStr
for b2 being Subset-Family of R holds
( b2 = Classes R iff for A being Subset of R holds
( A in b2 iff ex a being Element of R st A = Class a ) );
theorem Th21:
:: deftheorem Def7 defines Am GCD_1:def 7 :
for R being non empty associative well-unital multLoopStr
for b2 being non empty Subset of R holds
( b2 is Am of R iff ( ( for a being Element of R ex z being Element of b2 st z is_associated_to a ) & ( for x, y being Element of b2 st x <> y holds
x is_not_associated_to y ) ) );
:: deftheorem Def8 defines AmpleSet GCD_1:def 8 :
for R being non empty associative well-unital multLoopStr
for b2 being non empty Subset of R holds
( b2 is AmpleSet of R iff ( b2 is Am of R & 1. R in b2 ) );
theorem Th22:
theorem
theorem Th24:
:: deftheorem Def9 defines NF GCD_1:def 9 :
for R being non empty associative well-unital multLoopStr
for Amp being AmpleSet of R
for x, b4 being Element of R holds
( b4 = NF x,Amp iff ( b4 in Amp & b4 is_associated_to x ) );
theorem Th25:
theorem
:: deftheorem Def10 defines multiplicative GCD_1:def 10 :
for R being non empty associative well-unital multLoopStr
for Amp being AmpleSet of R holds
( Amp is multiplicative iff for x, y being Element of Amp holds x * y in Amp );
theorem Th27:
begin
:: deftheorem Def11 defines gcd-like GCD_1:def 11 :
for R being non empty multLoopStr holds
( R is gcd-like iff for x, y being Element of R ex z being Element of R st
( z divides x & z divides y & ( for zz being Element of R st zz divides x & zz divides y holds
zz divides z ) ) );
:: deftheorem Def12 defines gcd GCD_1:def 12 :
for R being non empty associative well-unital gcd-like multLoopStr
for Amp being AmpleSet of R
for x, y, b5 being Element of R holds
( b5 = gcd x,y,Amp iff ( b5 in Amp & b5 divides x & b5 divides y & ( for z being Element of R st z divides x & z divides y holds
z divides b5 ) ) );
theorem
canceled;
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
for
R being
gcdDomain for
Amp being
AmpleSet of
R for
a,
b,
c being
Element of
R st
b is_associated_to c holds
(
gcd a,
b,
Amp is_associated_to gcd a,
c,
Amp &
gcd b,
a,
Amp is_associated_to gcd c,
a,
Amp )
theorem Th36:
for
R being
gcdDomain for
Amp being
AmpleSet of
R for
a,
b,
c being
Element of
R holds
gcd (gcd a,b,Amp),
c,
Amp = gcd a,
(gcd b,c,Amp),
Amp
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
begin
theorem Th41:
for
R being
gcdDomain for
Amp being
AmpleSet of
R for
r1,
r2,
s1,
s2 being
Element of
R st
gcd r1,
r2,
Amp = 1. R &
gcd s1,
s2,
Amp = 1. R &
r2 <> 0. R holds
gcd ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))),
(r2 * (s2 / (gcd r2,s2,Amp))),
Amp = gcd ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))),
(gcd r2,s2,Amp),
Amp
theorem Th42:
for
R being
gcdDomain for
Amp being
AmpleSet of
R for
r1,
r2,
s1,
s2 being
Element of
R st
gcd r1,
r2,
Amp = 1. R &
gcd s1,
s2,
Amp = 1. R &
r2 <> 0. R &
s2 <> 0. R holds
gcd ((r1 / (gcd r1,s2,Amp)) * (s1 / (gcd s1,r2,Amp))),
((r2 / (gcd s1,r2,Amp)) * (s2 / (gcd r1,s2,Amp))),
Amp = 1. R
begin
:: deftheorem Def13 defines are_canonical_wrt GCD_1:def 13 :
for R being non empty associative well-unital gcd-like multLoopStr
for Amp being AmpleSet of R
for x, y being Element of R holds
( x,y are_canonical_wrt Amp iff gcd x,y,Amp = 1. R );
theorem Th43:
:: deftheorem Def14 defines are_co-prime GCD_1:def 14 :
for R being non empty associative well-unital gcd-like multLoopStr
for x, y being Element of R holds
( x,y are_co-prime iff ex Amp being AmpleSet of R st gcd x,y,Amp = 1. R );
theorem Th44:
:: deftheorem Def15 defines are_normalized_wrt GCD_1:def 15 :
for R being non empty associative well-unital gcd-like multLoopStr_0
for Amp being AmpleSet of R
for x, y being Element of R holds
( x,y are_normalized_wrt Amp iff ( gcd x,y,Amp = 1. R & y in Amp & y <> 0. R ) );
definition
let R be
gcdDomain;
let Amp be
AmpleSet of
R;
let r1,
r2,
s1,
s2 be
Element of
R;
assume that A1:
r1,
r2 are_co-prime
and A2:
s1,
s2 are_co-prime
and A3:
r2 = NF r2,
Amp
and A4:
s2 = NF s2,
Amp
;
func add1 r1,
r2,
s1,
s2,
Amp -> Element of
R equals :
Def16:
s1 if r1 = 0. Rr1 if s1 = 0. R(r1 * s2) + (r2 * s1) if gcd r2,
s2,
Amp = 1. R 0. R if (r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp))) = 0. R otherwise ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))) / (gcd ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))),(gcd r2,s2,Amp),Amp);
coherence
( ( r1 = 0. R implies s1 is Element of R ) & ( s1 = 0. R implies r1 is Element of R ) & ( gcd r2,s2,Amp = 1. R implies (r1 * s2) + (r2 * s1) is Element of R ) & ( (r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp))) = 0. R implies 0. R is Element of R ) & ( not r1 = 0. R & not s1 = 0. R & not gcd r2,s2,Amp = 1. R & not (r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp))) = 0. R implies ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))) / (gcd ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))),(gcd r2,s2,Amp),Amp) is Element of R ) )
;
consistency
for b1 being Element of R holds
( ( r1 = 0. R & s1 = 0. R implies ( b1 = s1 iff b1 = r1 ) ) & ( r1 = 0. R & gcd r2,s2,Amp = 1. R implies ( b1 = s1 iff b1 = (r1 * s2) + (r2 * s1) ) ) & ( r1 = 0. R & (r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp))) = 0. R implies ( b1 = s1 iff b1 = 0. R ) ) & ( s1 = 0. R & gcd r2,s2,Amp = 1. R implies ( b1 = r1 iff b1 = (r1 * s2) + (r2 * s1) ) ) & ( s1 = 0. R & (r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp))) = 0. R implies ( b1 = r1 iff b1 = 0. R ) ) & ( gcd r2,s2,Amp = 1. R & (r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp))) = 0. R implies ( b1 = (r1 * s2) + (r2 * s1) iff b1 = 0. R ) ) )
end;
:: deftheorem Def16 defines add1 GCD_1:def 16 :
for R being gcdDomain
for Amp being AmpleSet of R
for r1, r2, s1, s2 being Element of R st r1,r2 are_co-prime & s1,s2 are_co-prime & r2 = NF r2,Amp & s2 = NF s2,Amp holds
( ( r1 = 0. R implies add1 r1,r2,s1,s2,Amp = s1 ) & ( s1 = 0. R implies add1 r1,r2,s1,s2,Amp = r1 ) & ( gcd r2,s2,Amp = 1. R implies add1 r1,r2,s1,s2,Amp = (r1 * s2) + (r2 * s1) ) & ( (r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp))) = 0. R implies add1 r1,r2,s1,s2,Amp = 0. R ) & ( not r1 = 0. R & not s1 = 0. R & not gcd r2,s2,Amp = 1. R & not (r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp))) = 0. R implies add1 r1,r2,s1,s2,Amp = ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))) / (gcd ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))),(gcd r2,s2,Amp),Amp) ) );
definition
let R be
gcdDomain;
let Amp be
AmpleSet of
R;
let r1,
r2,
s1,
s2 be
Element of
R;
assume that A1:
r1,
r2 are_co-prime
and A2:
s1,
s2 are_co-prime
and A3:
r2 = NF r2,
Amp
and A4:
s2 = NF s2,
Amp
;
func add2 r1,
r2,
s1,
s2,
Amp -> Element of
R equals :
Def17:
s2 if r1 = 0. Rr2 if s1 = 0. Rr2 * s2 if gcd r2,
s2,
Amp = 1. R 1. R if (r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp))) = 0. R otherwise (r2 * (s2 / (gcd r2,s2,Amp))) / (gcd ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))),(gcd r2,s2,Amp),Amp);
coherence
( ( r1 = 0. R implies s2 is Element of R ) & ( s1 = 0. R implies r2 is Element of R ) & ( gcd r2,s2,Amp = 1. R implies r2 * s2 is Element of R ) & ( (r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp))) = 0. R implies 1. R is Element of R ) & ( not r1 = 0. R & not s1 = 0. R & not gcd r2,s2,Amp = 1. R & not (r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp))) = 0. R implies (r2 * (s2 / (gcd r2,s2,Amp))) / (gcd ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))),(gcd r2,s2,Amp),Amp) is Element of R ) )
;
consistency
for b1 being Element of R holds
( ( r1 = 0. R & s1 = 0. R implies ( b1 = s2 iff b1 = r2 ) ) & ( r1 = 0. R & gcd r2,s2,Amp = 1. R implies ( b1 = s2 iff b1 = r2 * s2 ) ) & ( r1 = 0. R & (r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp))) = 0. R implies ( b1 = s2 iff b1 = 1. R ) ) & ( s1 = 0. R & gcd r2,s2,Amp = 1. R implies ( b1 = r2 iff b1 = r2 * s2 ) ) & ( s1 = 0. R & (r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp))) = 0. R implies ( b1 = r2 iff b1 = 1. R ) ) & ( gcd r2,s2,Amp = 1. R & (r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp))) = 0. R implies ( b1 = r2 * s2 iff b1 = 1. R ) ) )
end;
:: deftheorem Def17 defines add2 GCD_1:def 17 :
for R being gcdDomain
for Amp being AmpleSet of R
for r1, r2, s1, s2 being Element of R st r1,r2 are_co-prime & s1,s2 are_co-prime & r2 = NF r2,Amp & s2 = NF s2,Amp holds
( ( r1 = 0. R implies add2 r1,r2,s1,s2,Amp = s2 ) & ( s1 = 0. R implies add2 r1,r2,s1,s2,Amp = r2 ) & ( gcd r2,s2,Amp = 1. R implies add2 r1,r2,s1,s2,Amp = r2 * s2 ) & ( (r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp))) = 0. R implies add2 r1,r2,s1,s2,Amp = 1. R ) & ( not r1 = 0. R & not s1 = 0. R & not gcd r2,s2,Amp = 1. R & not (r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp))) = 0. R implies add2 r1,r2,s1,s2,Amp = (r2 * (s2 / (gcd r2,s2,Amp))) / (gcd ((r1 * (s2 / (gcd r2,s2,Amp))) + (s1 * (r2 / (gcd r2,s2,Amp)))),(gcd r2,s2,Amp),Amp) ) );
theorem
for
R being
gcdDomain for
Amp being
AmpleSet of
R for
r1,
r2,
s1,
s2 being
Element of
R st
Amp is
multiplicative &
r1,
r2 are_normalized_wrt Amp &
s1,
s2 are_normalized_wrt Amp holds
add1 r1,
r2,
s1,
s2,
Amp,
add2 r1,
r2,
s1,
s2,
Amp are_normalized_wrt Amp
theorem
for
R being
gcdDomain for
Amp being
AmpleSet of
R for
r1,
r2,
s1,
s2 being
Element of
R st
r1,
r2 are_normalized_wrt Amp &
s1,
s2 are_normalized_wrt Amp holds
(add1 r1,r2,s1,s2,Amp) * (r2 * s2) = (add2 r1,r2,s1,s2,Amp) * ((r1 * s2) + (s1 * r2))
definition
let R be
gcdDomain;
let Amp be
AmpleSet of
R;
let r1,
r2,
s1,
s2 be
Element of
R;
func mult1 r1,
r2,
s1,
s2,
Amp -> Element of
R equals :
Def18:
0. R if (
r1 = 0. R or
s1 = 0. R )
r1 * s1 if (
r2 = 1. R &
s2 = 1. R )
(r1 * s1) / (gcd r1,s2,Amp) if (
s2 <> 0. R &
r2 = 1. R )
(r1 * s1) / (gcd s1,r2,Amp) if (
r2 <> 0. R &
s2 = 1. R )
otherwise (r1 / (gcd r1,s2,Amp)) * (s1 / (gcd s1,r2,Amp));
coherence
( ( ( r1 = 0. R or s1 = 0. R ) implies 0. R is Element of R ) & ( r2 = 1. R & s2 = 1. R implies r1 * s1 is Element of R ) & ( s2 <> 0. R & r2 = 1. R implies (r1 * s1) / (gcd r1,s2,Amp) is Element of R ) & ( r2 <> 0. R & s2 = 1. R implies (r1 * s1) / (gcd s1,r2,Amp) is Element of R ) & ( r1 = 0. R or s1 = 0. R or ( r2 = 1. R & s2 = 1. R ) or ( s2 <> 0. R & r2 = 1. R ) or ( r2 <> 0. R & s2 = 1. R ) or (r1 / (gcd r1,s2,Amp)) * (s1 / (gcd s1,r2,Amp)) is Element of R ) )
;
consistency
for b1 being Element of R holds
( ( ( r1 = 0. R or s1 = 0. R ) & r2 = 1. R & s2 = 1. R implies ( b1 = 0. R iff b1 = r1 * s1 ) ) & ( ( r1 = 0. R or s1 = 0. R ) & s2 <> 0. R & r2 = 1. R implies ( b1 = 0. R iff b1 = (r1 * s1) / (gcd r1,s2,Amp) ) ) & ( ( r1 = 0. R or s1 = 0. R ) & r2 <> 0. R & s2 = 1. R implies ( b1 = 0. R iff b1 = (r1 * s1) / (gcd s1,r2,Amp) ) ) & ( r2 = 1. R & s2 = 1. R & s2 <> 0. R & r2 = 1. R implies ( b1 = r1 * s1 iff b1 = (r1 * s1) / (gcd r1,s2,Amp) ) ) & ( r2 = 1. R & s2 = 1. R & r2 <> 0. R & s2 = 1. R implies ( b1 = r1 * s1 iff b1 = (r1 * s1) / (gcd s1,r2,Amp) ) ) & ( s2 <> 0. R & r2 = 1. R & r2 <> 0. R & s2 = 1. R implies ( b1 = (r1 * s1) / (gcd r1,s2,Amp) iff b1 = (r1 * s1) / (gcd s1,r2,Amp) ) ) )
end;
:: deftheorem Def18 defines mult1 GCD_1:def 18 :
for R being gcdDomain
for Amp being AmpleSet of R
for r1, r2, s1, s2 being Element of R holds
( ( ( r1 = 0. R or s1 = 0. R ) implies mult1 r1,r2,s1,s2,Amp = 0. R ) & ( r2 = 1. R & s2 = 1. R implies mult1 r1,r2,s1,s2,Amp = r1 * s1 ) & ( s2 <> 0. R & r2 = 1. R implies mult1 r1,r2,s1,s2,Amp = (r1 * s1) / (gcd r1,s2,Amp) ) & ( r2 <> 0. R & s2 = 1. R implies mult1 r1,r2,s1,s2,Amp = (r1 * s1) / (gcd s1,r2,Amp) ) & ( r1 = 0. R or s1 = 0. R or ( r2 = 1. R & s2 = 1. R ) or ( s2 <> 0. R & r2 = 1. R ) or ( r2 <> 0. R & s2 = 1. R ) or mult1 r1,r2,s1,s2,Amp = (r1 / (gcd r1,s2,Amp)) * (s1 / (gcd s1,r2,Amp)) ) );
definition
let R be
gcdDomain;
let Amp be
AmpleSet of
R;
let r1,
r2,
s1,
s2 be
Element of
R;
assume that A1:
r1,
r2 are_co-prime
and A2:
s1,
s2 are_co-prime
and A3:
r2 = NF r2,
Amp
and A4:
s2 = NF s2,
Amp
;
func mult2 r1,
r2,
s1,
s2,
Amp -> Element of
R equals :
Def19:
1. R if (
r1 = 0. R or
s1 = 0. R )
1. R if (
r2 = 1. R &
s2 = 1. R )
s2 / (gcd r1,s2,Amp) if (
s2 <> 0. R &
r2 = 1. R )
r2 / (gcd s1,r2,Amp) if (
r2 <> 0. R &
s2 = 1. R )
otherwise (r2 / (gcd s1,r2,Amp)) * (s2 / (gcd r1,s2,Amp));
coherence
( ( ( r1 = 0. R or s1 = 0. R ) implies 1. R is Element of R ) & ( r2 = 1. R & s2 = 1. R implies 1. R is Element of R ) & ( s2 <> 0. R & r2 = 1. R implies s2 / (gcd r1,s2,Amp) is Element of R ) & ( r2 <> 0. R & s2 = 1. R implies r2 / (gcd s1,r2,Amp) is Element of R ) & ( r1 = 0. R or s1 = 0. R or ( r2 = 1. R & s2 = 1. R ) or ( s2 <> 0. R & r2 = 1. R ) or ( r2 <> 0. R & s2 = 1. R ) or (r2 / (gcd s1,r2,Amp)) * (s2 / (gcd r1,s2,Amp)) is Element of R ) )
;
consistency
for b1 being Element of R holds
( ( ( r1 = 0. R or s1 = 0. R ) & r2 = 1. R & s2 = 1. R implies ( b1 = 1. R iff b1 = 1. R ) ) & ( ( r1 = 0. R or s1 = 0. R ) & s2 <> 0. R & r2 = 1. R implies ( b1 = 1. R iff b1 = s2 / (gcd r1,s2,Amp) ) ) & ( ( r1 = 0. R or s1 = 0. R ) & r2 <> 0. R & s2 = 1. R implies ( b1 = 1. R iff b1 = r2 / (gcd s1,r2,Amp) ) ) & ( r2 = 1. R & s2 = 1. R & s2 <> 0. R & r2 = 1. R implies ( b1 = 1. R iff b1 = s2 / (gcd r1,s2,Amp) ) ) & ( r2 = 1. R & s2 = 1. R & r2 <> 0. R & s2 = 1. R implies ( b1 = 1. R iff b1 = r2 / (gcd s1,r2,Amp) ) ) & ( s2 <> 0. R & r2 = 1. R & r2 <> 0. R & s2 = 1. R implies ( b1 = s2 / (gcd r1,s2,Amp) iff b1 = r2 / (gcd s1,r2,Amp) ) ) )
end;
:: deftheorem Def19 defines mult2 GCD_1:def 19 :
for R being gcdDomain
for Amp being AmpleSet of R
for r1, r2, s1, s2 being Element of R st r1,r2 are_co-prime & s1,s2 are_co-prime & r2 = NF r2,Amp & s2 = NF s2,Amp holds
( ( ( r1 = 0. R or s1 = 0. R ) implies mult2 r1,r2,s1,s2,Amp = 1. R ) & ( r2 = 1. R & s2 = 1. R implies mult2 r1,r2,s1,s2,Amp = 1. R ) & ( s2 <> 0. R & r2 = 1. R implies mult2 r1,r2,s1,s2,Amp = s2 / (gcd r1,s2,Amp) ) & ( r2 <> 0. R & s2 = 1. R implies mult2 r1,r2,s1,s2,Amp = r2 / (gcd s1,r2,Amp) ) & ( r1 = 0. R or s1 = 0. R or ( r2 = 1. R & s2 = 1. R ) or ( s2 <> 0. R & r2 = 1. R ) or ( r2 <> 0. R & s2 = 1. R ) or mult2 r1,r2,s1,s2,Amp = (r2 / (gcd s1,r2,Amp)) * (s2 / (gcd r1,s2,Amp)) ) );
theorem
for
R being
gcdDomain for
Amp being
AmpleSet of
R for
r1,
r2,
s1,
s2 being
Element of
R st
Amp is
multiplicative &
r1,
r2 are_normalized_wrt Amp &
s1,
s2 are_normalized_wrt Amp holds
mult1 r1,
r2,
s1,
s2,
Amp,
mult2 r1,
r2,
s1,
s2,
Amp are_normalized_wrt Amp
theorem
for
R being
gcdDomain for
Amp being
AmpleSet of
R for
r1,
r2,
s1,
s2 being
Element of
R st
r1,
r2 are_normalized_wrt Amp &
s1,
s2 are_normalized_wrt Amp holds
(mult1 r1,r2,s1,s2,Amp) * (r2 * s2) = (mult2 r1,r2,s1,s2,Amp) * (r1 * s1)
theorem
canceled;
theorem
canceled;
theorem
theorem
canceled;
theorem