feat(ring_theory/fractional_ideal): helper lemmas for Dedekind domains (

#4994)

An assortment of lemmas and refactoring related to `fractional_ideal`s, 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_ring`s
 * `algebra A (fraction_ring A)` instance

Overview of the changes in `fractional_ideal.lean`:
 * generalize many lemmas from integral domains to (nontrivial) `comm_ring`s (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>



Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>