fact: Definition fpsring ( R : commring ) := make_setwith2binop ( make_hSet ( seqson R ) ( isasetfps R ) ) ( make_dirprod ( fpsplus R ) ( fpstimes R ) ).
imports: UniMath.PAdics.lemmas UniMath.Algebra.RigsAndRings UniMath.NumberSystems.Integers