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 Central element [ add ] Algebra.Definitions.Central plus Consequences for Identity and Zero #2873
• 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? #2885

[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!