environ
vocabularies HIDDEN, XBOOLE_0, STRUCT_0, SUBSET_1, ZFMISC_1, SUPINF_2, ALGSTR_0, MESFUNC1, MCART_1, VECTSP_2, RELAT_1, ARYTM_3, BINOP_1, RLVECT_1, LATTICES, SETFAM_1, FUNCSDOM, GROUP_1, ARYTM_1, FUNCT_1, VECTSP_1, MSSUBFAM, TARSKI, QUOFIELD, FUNCT_2, FDIFF_1, MOD_4;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, XTUPLE_0, MCART_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, SETFAM_1, BINOP_1, DOMAIN_1, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_2, VECTSP_1, TOPS_2, GRCAT_1, GCD_1, GROUP_6, RINGCAT1, MOD_4;
definitions VECTSP_1, VECTSP_2, XBOOLE_0, ALGSTR_0;
theorems TARSKI, VECTSP_1, VECTSP_2, SUBSET_1, BINOP_1, RLVECT_1, FUNCT_1, FUNCT_2, GCD_1, RELAT_1, RELSET_1, TOPS_2, XBOOLE_0, GROUP_1, GROUP_6, STRUCT_0, XTUPLE_0;
schemes SUBSET_1, BINOP_1, FUNCT_2;
registrations SUBSET_1, RELSET_1, FUNCT_2, STRUCT_0, VECTSP_1, ALGSTR_1, GCD_1, XTUPLE_0, RINGCAT1, MOD_4;
constructors HIDDEN, DOMAIN_1, TOPS_2, GRCAT_1, GROUP_6, GCD_1, ALGSTR_1, RELSET_1, XTUPLE_0, RINGCAT1, MOD_4;
requirements HIDDEN, SUBSET, BOOLE;
equalities STRUCT_0, XBOOLE_0, ALGSTR_0;
expansions VECTSP_1, XBOOLE_0, FUNCT_2, RINGCAT1, MOD_4;
definition
let I be non
degenerated commutative domRing-like Ring;
existence
ex b1 being BinOp of (Quot. I) st
for u, v being Element of Quot. I holds b1 . (u,v) = qadd (u,v)
uniqueness
for b1, b2 being BinOp of (Quot. I) st ( for u, v being Element of Quot. I holds b1 . (u,v) = qadd (u,v) ) & ( for u, v being Element of Quot. I holds b2 . (u,v) = qadd (u,v) ) holds
b1 = b2
end;
definition
let I be non
degenerated commutative domRing-like Ring;
existence
ex b1 being BinOp of (Quot. I) st
for u, v being Element of Quot. I holds b1 . (u,v) = qmult (u,v)
uniqueness
for b1, b2 being BinOp of (Quot. I) st ( for u, v being Element of Quot. I holds b1 . (u,v) = qmult (u,v) ) & ( for u, v being Element of Quot. I holds b2 . (u,v) = qmult (u,v) ) holds
b1 = b2
end;
Lm1:
for I being non degenerated commutative domRing-like Ring holds
( the_Field_of_Quotients I is add-associative & the_Field_of_Quotients I is right_zeroed & the_Field_of_Quotients I is right_complementable )
Lm2:
for I being non degenerated commutative domRing-like Ring holds the_Field_of_Quotients I is non empty commutative doubleLoopStr
Lm3:
for I being non degenerated commutative domRing-like Ring holds the_Field_of_Quotients I is well-unital
by Th25;