mathlib

d6420bdc - 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]`.