chore(RingTheory/Ideal): add new file `Ideal.IsPrincipal`

[xroblot]

This PR adds a new file RingTheory.Ideal.IsPrincipal and moves most of the (basic) results about Ideal.IsPrincipal and Ideal.span_singleton from Ideal.Basic and Ideal.Operations to this file. (Some very basic results or results related to Submodule.span_singleton are left in place.)

The need for this PR comes from a discussion in #12780 about where to put the proof that the equivalence between principal ideals and associates is actually a MulEquiv (#13177).

Some remarks:

• no_lost_declarations.sh says

* 25  added declarations
* 25  removed declarations
* 5  paired declarations

this is due to some renames in the variables and also namespace changes. I have checked that the added declarations correspond exactly to the removed declarations

• Some results that could not stay in Ideal.Basic but are not really related to principal ideals have been moved (for the moment?) to the end of Ideal.IsPrincipal (see the misc section). I thought about putting them in Ideal.Operations but the file is already quite large (about 1400 lines). Note that Ideal.Operations imports Ideal.IsPrincipal and these additional results do not add any extra import to Ideal.IsPrincipal. Still, they should probably go somewhere else...

---