feat(Ideal.IsPrincipal): Prove that the equiv between principal ideals and associates is a `MulEquiv`

[xroblot]

Define the Submonoid of principal ideals and prove that associatesEquivIsPrincipal : Associates R ≃ {I : Ideal R // Submodule.IsPrincipal I} actually yields a MulEquiv between Associates R and this Submonoid.

---

• [ ] depends on: #13175

[mergify[bot]]

⚠️ The sha of the head commit of this PR conflicts with #13175. Mergify cannot evaluate rules on this PR. ⚠️

[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
• Check all files imported
• Lint style