feat(ring_theory/principal_ideal_domain): definition of principal submodule (#2761)
feat(ring_theory/principal_ideal_domain): definition of principal submodule (#2761)

This PR generalizes the definition of principal ideals to principal submodules. It turns out that it's essentially enough to replace `ideal R` with `submodule R M` in the relevant places. With this change, it's possible to talk about principal fractional ideals (although that development will have to wait #2714 gets merged).

Since the PR already changes the variables used in this file, I took the opportunity to rename them so `[ring α]` becomes `[ring R]`.



leanprover-community/mathlib,leanprover-community/mathlib