Add principal ideal construction

[Taneb]

On top of #2855, taken from #2729

[jamesmckinna]

As with the (admittedly fiddly) factorisation of the Binomial Theorem in #1928 , consider refactoring this so that:

• the principal ideal of a general Ring is well-defined for any element which commutes with everything in the ring
• hence, for a CommutativeRing, the principal ideal is always well-defined.

UPDATED: might usefully need to define the Centre Center of an algebra, commutator subgroup of a group, ... etc. as free-standing concepts, for subsequent (refactored) deployment in this context? #2863

[Taneb]

As with the (admittedly fiddly) factorisation of the Binomial Theorem, consider refactoring this so that:

* the principal ideal of a general `Ring` is well-defined for _any_ element which commutes with everything in the ring

* hence, for a `CommutativeRing`, the principal ideal is _always_ well-defined.

To help justify this to future me who may have forgotten this, the scalar multiples of the identity matrix commute with all square matrices (over a commutative ring)

[JacquesCarette]

I know it's still draft, I'm still approving!

[jamesmckinna]

Can these be recreated by record { RawBimodule rawBimodule hiding (_≈ᴹ_); _≈ᴹ_ = _≈_ on a *_ }, with rawBimodule brought into scope by the opening of subbimodule in Ideal?

[jamesmckinna]

Can we even lift out the definition ι = a *_ in a where clause, so that this could 'just' be _≈ᴹ_ = _≈_ on ι ?

[jamesmckinna]

... and here?

[jamesmckinna]

Is there nothing under Algebra.Properties.(Commutative)Semigroup that could be deployed here, as on the previous line, mentioning only a?

[Taneb]

I don't think so, and certainly not with this argument order