Splitting `localization.lean` and `dedekind_domain.lean

Stream: general

[Anne Baanen]

Some files in ring_theory, especially localization.lean and dedekind_domain.lean are a couple thousand lines long and have a huge set of transitive dependencies. I'd like to add a couple of lemmas to those files, but it takes ages to compile currently. Anyone opposed to carving these files up into smaller pieces (with hopefully smaller imports)?

[Anne Baanen]

I'm thinking:

• dedekind_domain/basic.lean: definition of is_dedekind_domain, basic lemmas
• dedekind_domain/ideal.lean: show that is_dedekind_domain iff all fractional ideals are invertible; unique factorization of ideals
• dedekind_domain/dvr.lean: currently just is_dedekind_domain_dvr, would be the place to add that equivalence

• dedekind_domain/integral_closure.lean: show that the integral closure in a finite separable extension is a Dedekind domain

• localization/basic.lean: definition of is_localization, is_localization.away; is_localization.at_prime, is_fraction_ring; comm_ring and field instances; lift; mk; alg_equiv (the .away, .at_prime and fraction_ring parts might deserve their own files)

• localization/integer.lean: is_integer; exist_integer_multiples
• localization/num_denom.lean: common_denom; num; denom
• localization/submodule.lean: coe_submodule
• localization/ideal.lean: is_localization.map_ideal, some of the ideal.quotient_map results

[Eric Rodriguez]

I was going to add localization.cardinality soon (tiny file, but still), so this is timely and seems like a good idea!

[Anne Baanen]

Thanks to @Alex J. Best and @Johan Commelin's import tool, the import graph has been halved from 832 transitive imports to 409! #12206

[Yaël Dillies]

Wow, this has to be one of the biggest PR ever!