Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I guess one could apply the definition in the case that for every pair of elements there is a unique such that either or . Then it makes sense to define iff such is invertible. This assumption should probably hold if the map to the ring completion is injective, which seems to require that the additive monoid is cancellative.
One might demand that addition is cancellative in a general division rig, and I guess this might be enough to arrive at the definition otherwise involving subtraction. Or else add this as an explicit hypothesis to this definition, assuming it works.
1 to 4 of 4