Definition ismultmonoidfuntofldfrac (X : intdom) (is : isdeceq X) : @ismonoidfun (ringmultmonoid X) (ringmultmonoid (fldfrac X is)) (tofldfrac X is) := isbinop2funtofldfrac X is ,, isunital2funtofldfrac X is.
Require Import UniMath.Algebra.Groups.