Definition ismultmonoidfuntoringdiff (X : rig) : @ismonoidfun (rigmultmonoid X) (ringmultmonoid (rigtoring X)) (toringdiff X) := isbinop2funtoringdiff X ,, isunital2funtoringdiff X.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.