# Zulip Chat Archive

## Stream: general

### Topic: Splitting `localization.lean` and `dedekind_domain.lean

#### Anne Baanen (Feb 21 2022 at 12:42):

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 (Feb 21 2022 at 12:43):

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 (Feb 21 2022 at 12:46):

I was going to add `localization.cardinality`

soon (tiny file, but still), so this is timely and seems like a good idea!

#### Anne Baanen (Feb 22 2022 at 10:20):

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 (Feb 22 2022 at 10:27):

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

Last updated: Aug 03 2023 at 10:10 UTC