Remove redundant fields from Ring

[Alizter]

In Ring we ask that the carrier be an abelian group and we also ask for the entire thing to be a ring. This ends up with having duplicated assumptions on the underlying abelian group. It doesn't affect anything in practice since these are all equal as hprops, but it does mean some terms might not unify as expected.

See #1921