Definition isringfuntofldfrac (X : intdom) (is : isdeceq X) : @isringfun X (fldfrac X is) (tofldfrac X is) := isaddmonoidfuntofldfrac X is ,, ismultmonoidfuntofldfrac X is.
Require Import UniMath.Algebra.Groups.