Commit 2020-11-17 12:21 7a707646

feat(ring_theory/fractional_ideal): helper lemmas for Dedekind domains (#4994) An assortment of lemmas and refactoring related to fractional_ideals, used in the Dedekind domain project.

The motivation for creating this PR is that we are planning to remove the general has_inv instance on fractional_ideal (reserving it only for Dedekind domains), and we don't want to do the resulting refactoring twice. So we make sure everything is in the master branch, do the refactoring there, then merge the changes back into the work in progress branch. Overview of the changes in localization.lean:

• more is_integer lemmas
• a localization of a noetherian ring is noetherian
• generalize a few lemmas from integral domains to nontrivial comm_rings
• algebra A (fraction_ring A) instance Overview of the changes in fractional_ideal.lean:
• generalize many lemmas from integral domains to (nontrivial) comm_rings (now R is notation for a comm_ring and R₁ for an integral domain)
• is_fractional_of_le, is_fractional_span_iff and is_fractional_of_fg
• many simp and norm_cast results involving coe : ideal -> fractional_ideal and coe : fractional_ideal -> submodule: now should be complete for 0, 1, +, *, / and ≤.
• use 1 : submodule as simp normal form instead of coe_submodule (1 : ideal)
• make the multiplication operation irreducible
• port submodule.has_mul lemmas to fractional_ideal.has_mul
• simp lemmas for canonical_equiv, span_singleton
• many ways to prove is_noetherian Co-Authored-By: Ashvni ashvni.n@gmail.com Co-Authored-By: faenuccio filippo.nuccio@univ-st-etienne.fr