fact: Definition fldfracmultinv0 (X : intdom) (is : isdeceq X) (x : commringfrac X (intdomnonzerosubmonoid X)) : commringfrac X (intdomnonzerosubmonoid X) := setquotfun _ _ _ (fldfracmultinvintcomp X is) x.
imports: UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings