feat: add a version of `Ideal.associatesEquivIsPrincipal` for generators that are non-zero-divisors

[xroblot]

trafficstars

This PR defines the following equiv:

def Ideal.associatesNonZeroDivisorsEquivIsPrincipal : 
    Associates R⁰ ≃ {I : (Ideal R)⁰ // IsPrincipal (I : Ideal R)}

Also, move the definition Ideal.associatesEquivIsPrincipal from Ideal.Basic to Ideal.Maps.

---

• [x] depends on: #12768
• [x] depends on: #12777
• [ ] depends on: #13177

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#12768~~
• ~~leanprover-community/mathlib4#12777~~
• ~~leanprover-community/mathlib4#13177~~ By Dependent Issues (🤖). Happy coding!

[github-actions[bot]]

PR summary 5efc615858

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ Ideal.span_singleton_nonZeroDivisors + associatesNonZeroDivisorsEquivIsPrincipal + associatesNonZeroDivisorsEquivIsPrincipal_apply + associatesNonZeroDivisorsEquivIsPrincipal_coe + associatesNonZeroDivisorsEquivIsPrincipal_map_one + associatesNonZeroDivisorsEquivIsPrincipal_mul + associatesNonZeroDivisorsMulEquivIsPrincipal + isPrincipalNonZeroDivisorsSubmonoid

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[riccardobrasca]

Thanks!

bors d+

[mathlib-bors[bot]]

:v: xroblot can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[xroblot]

bors r+

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style