Ring reasoning

[JacquesCarette]

Reasoning combinators for monoid, renamed and adapted for Ring. Builds on #2692 .

[Taneb]

1. I'd like to see the new semigroup properties here as well
2. The semigroup properties on * and the monoid properties on + work for RingWithoutOne
3. In fact, they work on Semiring and SemiringWithoutOne, but we don't have a Properties module for those

[jamesmckinna]

@Taneb 's 1,2,3 above echo my thoughts on looking at these, but maybe, given our ongoing issues regarding naming in #2688 that it isn't so straightforward to back-fill the Properties for weaker structures... yet?

[jamesmckinna]

Thanks for incorporating my nitpick suggestions.

[jamesmckinna]

Guessing that this PR hints that we should perhaps also have/need the intermediate extension to Algebra.Properties.(Abelian)Group to incorporate inverse equational simplification for the +-abelianGroup sub-structure/-bundle... as a downstream PR.

[JacquesCarette]

Yes, there is quite a lot that can be done in this vein.

We should be careful not to have perfect be the enemy of definite-improvement...

[jamesmckinna]

Yes, there is quite a lot that can be done in this vein.

We should be careful not to have perfect be the enemy of definite-improvement...

Yeah, not my intention at all to obstruct this PR with demands for more here... but elsewhere, in due course, definitely!

[JacquesCarette]

I guess, strictly speaking, neither you nor @Taneb are blocking this on requiring more features...

[jamesmckinna]

Absolutely not blocking from me!

but... maybe a rebase against the new master to sort out the CHANGELOG conflict, and to catch the already-merged Semigroup commits (I think the Monoid PR I still open though...?)?

[JacquesCarette]

That's why it's Draft, I need to do at least those changes.

[jamesmckinna]

Suggest a rebase to bring this up-to-date with everything that has happened so far, esp. if you want this for v2.4
Otherwise looks fine (though I personally don't like 'short' qualified module names such as PM, rather than eg MonoidProperties), as I don't really see that saving characters is the win worth having, compared to not having to chase at least one level of indirection to figure out what is going on... but then I'm on the 'verbose' end of the spectrum ;-)

[jamesmckinna]

@JacquesCarette If you fix up the merge conflicts, happy to merge this in.
Happy to fix the merge conflicts, if you prefer, or don't currently have time!

[jamesmckinna]

After rebasing against current master versions of Algebra.Properties.Monoid, this should better be:

Suggested change

	renaming ( ε-unique to 0#-unique; ε-comm to 0#-comm
	renaming ( ε-unique to 0#-unique; ε-central to 0#-central

[jamesmckinna]

Ditto

Suggested change

	renaming ( ε-unique to 1#-unique; ε-comm to 1#-comm
	renaming ( ε-unique to 1#-unique; ε-central to 1#-central

[jamesmckinna]

As with #2851 could we aim to finish this for v2.4, and then take stock/rationalise/refactor as part of the larger-scale breaking changes planned for v3.)

[JacquesCarette]

Yes, I'll try to deal with the conflicts soon. First, I need to catch up on what's been going on in stdlib!