Add IsRingWithoutOne and RingWithoutOne

[Taneb]

These are useful for talking about ideals of rings, which in general have this form.

[Akshobhya1234]

@Taneb Is it Rng as defined here? If required I can migrate it to stdlib

record IsRng (+ * : Op₂ A) (-_ : Op₁ A) (0# : A) : Set (a ⊔ ℓ) where
field
+-isAbelianGroup : IsAbelianGroup + 0# -_
*-isSemigroup : IsSemigroup *
distrib : * DistributesOver +
zero : Zero 0# *

https://github.com/Akshobhya1234/Agda-Algebra/blob/c358d3aa0179a9b6e287d2a06b184856b081d721/src/Structures.agda#L23-L28

[Taneb]

@Akshobhya1234 yes, that looks right, but note the changes in #1684

[Akshobhya1234]

@MatthewDaggitt or @Taneb I think we can close this issue. Or is there something that is still missing?

[MatthewDaggitt]

Yes, you're right! I forgot to link the PR to the issue. Thanks for the heads up!