Commit 2020-05-20 15:35 d6420bdc

View on Github →

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

Estimated changes

Modified src/ring_theory/principal_ideal_domain.lean

deleted theorem ideal.is_principal.eq_bot_iff_generator_eq_zero

deleted theorem ideal.is_principal.generator_mem

deleted theorem ideal.is_principal.mem_iff_generator_dvd

deleted theorem ideal.is_principal.span_singleton_generator

modified theorem is_prime.to_maximal_ideal

modified theorem mod_mem_iff

modified theorem principal_ideal_domain.associates_irreducible_iff_prime

modified theorem principal_ideal_domain.factors_decreasing

modified theorem principal_ideal_domain.factors_spec

modified theorem principal_ideal_domain.irreducible_iff_prime

modified theorem principal_ideal_domain.is_maximal_of_irreducible

added theorem submodule.is_principal.eq_bot_iff_generator_eq_zero

added theorem submodule.is_principal.generator_mem

added theorem submodule.is_principal.mem_iff_eq_smul_generator

added theorem submodule.is_principal.mem_iff_generator_dvd

added theorem submodule.is_principal.span_singleton_generator