Replace AlgNb by IntgRing from @digama0 's mathbox

[tirix]

As discussed in #4578, this replaces AlgNb (algebraic numbers, defined by taking roots of nonzero polynomials) with IntgRing (integral elements of a ring, defined by taking roots of monic polynomials).

The new definition is more general, and as shown in irngnzply1, for fields, this is the same.

The definition df-irng of elements of a ring integral over a subring is moved from @digama0's mathbox into mine, but I did not update changes-set.txt as no theorem is moved. No theorem was previously developped based on this definition, I've added a few basic ones.

This is one (very small) step towards solving #4246.

PS. I've fixed a small mistake in @digama0's definition (the ( r evalSub1 s ) was missing in ( ( r evalSub1 s ) ` f )), so I've added a "Revised by" in the definition's comment.

[avekens]

Great, everything is fine now.