:: GCD_1 semantic presentation

registration

cluster non empty commutative right_unital -> non empty left_unital multLoopStr ;
coherence

proof end;

end;

registration

cluster non empty commutative right-distributive -> non empty distributive doubleLoopStr ;
coherence

proof end;

cluster non empty commutative left-distributive -> non empty distributive doubleLoopStr ;
coherence

proof end;

end;

registration

cluster -> unital doubleLoopStr ;
coherence ;

end;

registration

cluster F_Real -> domRing-like ;
coherence

proof end;

end;

registration

cluster non empty Abelian add-associative right_zeroed right_complementable unital associative commutative strict distributive Field-like non degenerated domRing-like doubleLoopStr ;
existence

proof end;

end;

theorem Th1: :: GCD_1:1

for R being commutative domRing-like Ring
for a, b, c being Element of R st a <> 0. R holds
( ( a * b = a * c implies b = c ) & ( b * a = c * a implies b = c ) )

proof end;

definition

let R be non empty HGrStr ;
let x, y be Element of R;
pred x divides y means :Def1: :: GCD_1:def 1
ex z being Element of R st y = x * z;

end;

:: deftheorem Def1 defines divides GCD_1:def 1 :

definition

let R be non empty unital multLoopStr ;
let x, y be Element of R;
:: original: divides
redefine pred x divides y;
reflexivity

proof end;

end;

definition

let R be non empty multLoopStr ;
let x be Element of R;
attr x is unital means :Def2: :: GCD_1:def 2
x divides 1. R;

end;

:: deftheorem Def2 defines unital GCD_1:def 2 :

definition

let R be non empty multLoopStr ;
let x, y be Element of R;
pred x is_associated_to y means :Def3: :: GCD_1:def 3
( x divides y & y divides x );
symmetry ;

end;

:: deftheorem Def3 defines is_associated_to GCD_1:def 3 :

notation

let R be non empty multLoopStr ;
let x, y be Element of R;
antonym x is_not_associated_to y for x is_associated_to y;

end;

definition

let R be non empty unital multLoopStr ;
let x, y be Element of R;
:: original: is_associated_to
redefine pred x is_associated_to y;
reflexivity

proof end;

end;

definition

let R be commutative domRing-like Ring;
let x, y be Element of R;
assume A1: y divides x ;
assume A2: y <> 0. R ;
func x / y -> Element of R means :Def4: :: GCD_1:def 4
it * y = x;
existence

proof end;

uniqueness by A2, Th1;

end;

:: deftheorem Def4 defines / GCD_1:def 4 :

theorem Th2: :: GCD_1:2

for R being non empty associative multLoopStr
for a, b, c being Element of R st a divides b & b divides c holds
a divides c

proof end;

theorem Th3: :: GCD_1:3

for R being non empty associative commutative multLoopStr
for a, b, c, d being Element of R st b divides a & d divides c holds
b * d divides a * c

proof end;

theorem Th4: :: GCD_1:4

for R being non empty associative multLoopStr
for a, b, c being Element of R st a is_associated_to b & b is_associated_to c holds
a is_associated_to c

proof end;

theorem Th5: :: GCD_1:5

for R being non empty associative multLoopStr
for a, b, c being Element of R st a divides b holds
c * a divides c * b

proof end;

theorem Th6: :: GCD_1:6

for R being non empty multLoopStr
for a, b being Element of R holds
( a divides a * b & ( R is commutative implies b divides a * b ) )

proof end;

theorem Th7: :: GCD_1:7

for R being non empty associative multLoopStr
for a, b, c being Element of R st a divides b holds
a divides b * c

proof end;

theorem Th8: :: GCD_1:8

for R being commutative domRing-like Ring
for a, b being Element of R st b divides a & b <> 0. R holds
( a / b = 0. R iff a = 0. R )

proof end;

theorem Th9: :: GCD_1:9

for R being commutative domRing-like Ring
for a being Element of R st a <> 0. R holds
a / a = 1. R

proof end;

theorem Th10: :: GCD_1:10

for R being commutative non degenerated domRing-like Ring
for a being Element of R holds a / (1. R) = a

proof end;

theorem Th11: :: GCD_1:11

for R being commutative domRing-like Ring
for a, b, c being Element of R st c <> 0. R holds
( ( c divides a * b & c divides a implies (a * b) / c = (a / c) * b ) & ( c divides a * b & c divides b implies (a * b) / c = a * (b / c) ) )

proof end;

theorem Th12: :: GCD_1:12

for R being commutative domRing-like Ring
for a, b, c being Element of R st c <> 0. R & c divides a & c divides b & c divides a + b holds
(a / c) + (b / c) = (a + b) / c

proof end;

theorem :: GCD_1:13

for R being commutative domRing-like Ring
for a, b, c being Element of R st c <> 0. R & c divides a & c divides b holds
( a / c = b / c iff a = b )

proof end;

theorem Th14: :: GCD_1:14

for R being commutative domRing-like Ring
for a, b, c, d being Element of R st b <> 0. R & d <> 0. R & b divides a & d divides c holds
(a / b) * (c / d) = (a * c) / (b * d)

proof end;

theorem Th15: :: GCD_1:15

for R being commutative domRing-like Ring
for a, b, c being Element of R st a <> 0. R & a * b divides a * c holds
b divides c

proof end;

theorem :: GCD_1:16

for R being commutative domRing-like Ring
for a being Element of R st a is_associated_to 0. R holds
a = 0. R

proof end;

theorem Th17: :: GCD_1:17

for R being commutative domRing-like Ring
for a, b being Element of R st a <> 0. R & a * b = a holds
b = 1. R

proof end;

theorem Th18: :: GCD_1:18

for R being commutative domRing-like Ring
for a, b being Element of R holds
( a is_associated_to b iff ex c being Element of R st
( c is unital & a * c = b ) )

proof end;

theorem Th19: :: GCD_1:19

for R being commutative domRing-like Ring
for a, b, c being Element of R st c <> 0. R & c * a is_associated_to c * b holds
a is_associated_to b

proof end;

definition

let R be non empty multLoopStr ;
let a be Element of R;
func Class a -> Subset of R means :Def5: :: GCD_1:def 5
for b being Element of R holds
( b in it iff b is_associated_to a );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines Class GCD_1:def 5 :

registration

let R be non empty unital multLoopStr ;
let a be Element of R;
cluster Class a -> non empty ;
coherence

proof end;

end;

theorem Th20: :: GCD_1:20

for R being non empty associative multLoopStr
for a, b being Element of R st Class a meets Class b holds
Class a = Class b

proof end;

definition

let R be non empty multLoopStr ;
func Classes R -> Subset-Family of R means :Def6: :: GCD_1:def 6
for A being Subset of R holds
( A in it iff ex a being Element of R st A = Class a );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines Classes GCD_1:def 6 :

registration

let R be non empty multLoopStr ;
cluster Classes R -> non empty ;
coherence

proof end;

end;

theorem Th21: :: GCD_1:21

for R being non empty unital multLoopStr
for X being Subset of R st X in Classes R holds
not X is empty

proof end;

definition

let R be non empty unital associative multLoopStr ;
mode Am of R -> non empty Subset of R means :Def7: :: GCD_1:def 7
( ( for a being Element of R ex z being Element of it st z is_associated_to a ) & ( for x, y being Element of it st x <> y holds
x is_not_associated_to y ) );
existence

proof end;

end;

:: deftheorem Def7 defines Am GCD_1:def 7 :

definition

let R be non empty unital associative multLoopStr ;
mode AmpleSet of R -> non empty Subset of R means :Def8: :: GCD_1:def 8
( it is Am of R & 1. R in it );
existence

proof end;

end;

:: deftheorem Def8 defines AmpleSet GCD_1:def 8 :

theorem Th22: :: GCD_1:22

for R being non empty unital associative multLoopStr
for Amp being AmpleSet of R holds
( 1. R in Amp & ( for a being Element of R ex z being Element of Amp st z is_associated_to a ) & ( for x, y being Element of Amp st x <> y holds
x is_not_associated_to y ) )

proof end;

theorem :: GCD_1:23

for R being non empty unital associative multLoopStr
for Amp being AmpleSet of R
for x, y being Element of Amp st x is_associated_to y holds
x = y by Th22;

theorem Th24: :: GCD_1:24

for R being commutative domRing-like Ring
for Amp being AmpleSet of R holds 0. R is Element of Amp

proof end;

definition

let R be non empty unital associative multLoopStr ;
let Amp be AmpleSet of R;
let x be Element of R;
func NF x,Amp -> Element of R means :Def9: :: GCD_1:def 9
( it in Amp & it is_associated_to x );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines NF GCD_1:def 9 :

theorem Th25: :: GCD_1:25

for R being commutative domRing-like Ring
for Amp being AmpleSet of R holds
( NF (0. R),Amp = 0. R & NF (1. R),Amp = 1. R )

proof end;

theorem :: GCD_1:26

for R being commutative domRing-like Ring
for Amp being AmpleSet of R
for a being Element of R holds
( a in Amp iff a = NF a,Amp ) by Def9;

definition

let R be non empty unital associative multLoopStr ;
let Amp be AmpleSet of R;
attr Amp is multiplicative means :Def10: :: GCD_1:def 10
for x, y being Element of Amp holds x * y in Amp;

end;

:: deftheorem Def10 defines multiplicative GCD_1:def 10 :

theorem Th27: :: GCD_1:27

for R being commutative domRing-like Ring
for Amp being AmpleSet of R st Amp is multiplicative holds
for x, y being Element of Amp st y divides x & y <> 0. R holds
x / y in Amp

proof end;

definition

let R be non empty multLoopStr ;
attr R is gcd-like means :Def11: :: GCD_1:def 11
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 ) );

end;

:: deftheorem Def11 defines gcd-like GCD_1:def 11 :

Lm1: now

let F be Field; :: thesis:
let x, y be Element of F; :: thesis:

now

per cases ;

case A1: ( x <> 0. F & y <> 0. F ) ; :: thesis:

x = (1. F) * x by VECTSP_2:1;
then A2: 1. F divides x by Def1;
y = (1. F) * y by VECTSP_2:1;
then A3: 1. F divides y by Def1;
for zz being Element of F st zz divides x & zz divides y holds
zz divides 1. F

proof

let zz be Element of F; :: thesis:
assume A4: ( zz divides x & zz divides y ) ; :: thesis:

now

per cases ;

case zz <> 0. F ; :: thesis:

then consider zz' being Element of F such that
A5: zz * zz' = 1. F by VECTSP_1:def 20;
thus zz divides 1. F by A5, Def1; :: thesis:

end;

case A6: zz = 0. F ; :: thesis:

assume zz divides x ; :: thesis:
then consider d being Element of F such that
A7: zz * d = x by Def1;
thus zz divides 1. F by A1, A6, A7, VECTSP_1:39; :: thesis:

end;

hence zz divides 1. F by A4; :: thesis:

end;

hence ex z being Element of F st
( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds
zz divides z ) ) by A2, A3; :: thesis:

end;

case A8: x = 0. F ; :: thesis:

y * (0. F) = 0. F by VECTSP_1:39;
then A9: y divides 0. F by Def1;
for z being Element of F st z divides 0. F & z divides y holds
z divides y ;
hence ex z being Element of F st
( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds
zz divides z ) ) by A8, A9; :: thesis:

end;

case A10: y = 0. F ; :: thesis:

x * (0. F) = 0. F by VECTSP_1:39;
then A11: x divides 0. F by Def1;
for z being Element of F st z divides x & z divides 0. F holds
z divides x ;
hence ex z being Element of F st
( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds
zz divides z ) ) by A10, A11; :: thesis:

end;

hence ex z being Element of F st
( z divides x & z divides y & ( for zz being Element of F st zz divides x & zz divides y holds
zz divides z ) ) ; :: thesis:

end;

registration

cluster gcd-like doubleLoopStr ;
existence

proof end;

end;

registration

cluster non empty unital associative commutative gcd-like multLoopStr ;
existence

proof end;

end;

registration

cluster non empty unital associative commutative gcd-like multLoopStr_0 ;
existence

proof end;

end;

registration end;

registration

cluster non empty Abelian add-associative right_zeroed right_complementable unital associative commutative distributive non degenerated domRing-like gcd-like doubleLoopStr ;
existence

proof end;

end;

definition

mode gcdDomain is commutative non degenerated domRing-like gcd-like Ring;

end;

definition

let R be non empty unital associative gcd-like multLoopStr ;
let Amp be AmpleSet of R;
let x, y be Element of R;
func gcd x,y,Amp -> Element of R means :Def12: :: GCD_1:def 12
( it in Amp & it divides x & it divides y & ( for z being Element of R st z divides x & z divides y holds
z divides it ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines gcd GCD_1:def 12 :

theorem :: GCD_1:28

canceled;

theorem Th29: :: GCD_1:29

for R being gcdDomain
for Amp being AmpleSet of R
for a, b, c being Element of R st c divides gcd a,b,Amp holds
( c divides a & c divides b )

proof end;

theorem Th30: :: GCD_1:30

for R being gcdDomain
for Amp being AmpleSet of R
for a, b being Element of R holds gcd a,b,Amp = gcd b,a,Amp

proof end;

theorem Th31: :: GCD_1:31

for R being gcdDomain
for Amp being AmpleSet of R
for a being Element of R holds
( gcd a,(0. R),Amp = NF a,Amp & gcd (0. R),a,Amp = NF a,Amp )

proof end;

theorem Th32: :: GCD_1:32

for R being gcdDomain
for Amp being AmpleSet of R holds gcd (0. R),(0. R),Amp = 0. R

proof end;

theorem Th33: :: GCD_1:33

for R being gcdDomain
for Amp being AmpleSet of R
for a being Element of R holds
( gcd a,(1. R),Amp = 1. R & gcd (1. R),a,Amp = 1. R )

proof end;

theorem Th34: :: GCD_1:34

for R being gcdDomain
for Amp being AmpleSet of R
for a, b being Element of R holds
( gcd a,b,Amp = 0. R iff ( a = 0. R & b = 0. R ) )

proof end;

theorem Th35: :: GCD_1:35

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 )

proof end;

theorem Th36: :: GCD_1:36

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

proof end;

theorem Th37: :: GCD_1:37

for R being gcdDomain
for Amp being AmpleSet of R
for a, b, c being Element of R holds gcd (a * c),(b * c),Amp is_associated_to c * (gcd a,b,Amp)

proof end;

theorem Th38: :: GCD_1:38

for R being gcdDomain
for Amp being AmpleSet of R
for a, b, c being Element of R st gcd a,b,Amp = 1. R holds
gcd a,(b * c),Amp = gcd a,c,Amp

proof end;

theorem Th39: :: GCD_1:39

for R being gcdDomain
for Amp being AmpleSet of R
for a, b, c being Element of R st c = gcd a,b,Amp & c <> 0. R holds
gcd (a / c),(b / c),Amp = 1. R

proof end;

theorem Th40: :: GCD_1:40

for R being gcdDomain
for Amp being AmpleSet of R
for a, b, c being Element of R holds gcd (a + (b * c)),c,Amp = gcd a,c,Amp

proof end;

theorem Th41: :: GCD_1:41

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 * (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

proof end;

theorem Th42: :: GCD_1:42

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

proof end;

definition

let R be non empty unital associative gcd-like multLoopStr ;
let Amp be AmpleSet of R;
let x, y be Element of R;
pred x,y are_canonical_wrt Amp means :Def13: :: GCD_1:def 13
gcd x,y,Amp = 1. R;

end;

:: deftheorem Def13 defines are_canonical_wrt GCD_1:def 13 :

theorem Th43: :: GCD_1:43

for R being gcdDomain
for Amp, Amp' being AmpleSet of R
for x, y being Element of R holds
( x,y are_canonical_wrt Amp iff x,y are_canonical_wrt Amp' )

proof end;

definition

let R be non empty unital associative gcd-like multLoopStr ;
let x, y be Element of R;
pred x,y are_co-prime means :Def14: :: GCD_1:def 14
ex Amp being AmpleSet of R st gcd x,y,Amp = 1. R;

end;

:: deftheorem Def14 defines are_co-prime GCD_1:def 14 :

definition

let R be gcdDomain;
let x, y be Element of R;
:: original: are_co-prime
redefine pred x,y are_co-prime ;
symmetry

proof end;

end;

theorem Th44: :: GCD_1:44

for R being gcdDomain
for Amp being AmpleSet of R
for x, y being Element of R st x,y are_co-prime holds
gcd x,y,Amp = 1. R

proof end;

definition

let R be non empty unital associative gcd-like multLoopStr_0 ;
let Amp be AmpleSet of R;
let x, y be Element of R;
pred x,y are_normalized_wrt Amp means :Def15: :: GCD_1:def 15
( gcd x,y,Amp = 1. R & y in Amp & y <> 0. R );

end;

:: deftheorem Def15 defines are_normalized_wrt GCD_1:def 15 :

definition

let R be gcdDomain;
let Amp be AmpleSet of R;
let r1, r2, s1, s2 be Element of R;
assume A1: ( r1,r2 are_co-prime & s1,s2 are_co-prime & r2 = NF r2,Amp & s2 = NF s2,Amp ) ;
func add1 r1,r2,s1,s2,Amp -> Element of R equals :Def16: :: GCD_1:def 16
s1 if r1 = 0. R
r1 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 ;
consistency

proof end;

end;

:: deftheorem Def16 defines add1 GCD_1:def 16 :

definition

let R be gcdDomain;
let Amp be AmpleSet of R;
let r1, r2, s1, s2 be Element of R;
assume A1: ( r1,r2 are_co-prime & s1,s2 are_co-prime & r2 = NF r2,Amp & s2 = NF s2,Amp ) ;
func add2 r1,r2,s1,s2,Amp -> Element of R equals :Def17: :: GCD_1:def 17
s2 if r1 = 0. R
r2 if s1 = 0. R
r2 * 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 ;
consistency

proof end;

end;

:: deftheorem Def17 defines add2 GCD_1:def 17 :

theorem :: GCD_1:45

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

proof end;

theorem :: GCD_1:46

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) * (r2 * s2) = (add2 r1,r2,s1,s2,Amp) * ((r1 * s2) + (s1 * r2))

proof end;

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: :: GCD_1:def 18
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 ;
consistency

proof end;

end;

:: deftheorem Def18 defines mult1 GCD_1:def 18 :

definition

let R be gcdDomain;
let Amp be AmpleSet of R;
let r1, r2, s1, s2 be Element of R;
assume A1: ( r1,r2 are_co-prime & s1,s2 are_co-prime & r2 = NF r2,Amp & s2 = NF s2,Amp ) ;
func mult2 r1,r2,s1,s2,Amp -> Element of R equals :Def19: :: GCD_1:def 19
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 ;
consistency

proof end;

end;

:: deftheorem Def19 defines mult2 GCD_1:def 19 :

theorem :: GCD_1:47

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

proof end;

theorem :: GCD_1:48

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) * (r2 * s2) = (mult2 r1,r2,s1,s2,Amp) * (r1 * s1)

proof end;

theorem :: GCD_1:49

canceled;

theorem :: GCD_1:50

canceled;

theorem :: GCD_1:51

for F being non empty Abelian add-associative right_zeroed right_complementable distributive doubleLoopStr
for x, y being Element of F holds
( (- x) * y = - (x * y) & x * (- y) = - (x * y) ) by VECTSP_1:40, VECTSP_1:41;

theorem :: GCD_1:52

canceled;

theorem :: GCD_1:53

for F being commutative Field-like Ring
for a, b being Element of F st a <> 0. F & b <> 0. F holds
(a " ) * (b " ) = (b * a) "

proof end;