# Zulip Chat Archive

## Stream: general

### Topic: normalize

#### Kenny Lau (Feb 01 2019 at 12:21):

Ok this situation is quite complicated here and I'm not sure I understand the whole situation (an import graph would be quite beneficial).

So I look at algebra/gcd_domain.lean and think to myself: I should define `normalize x`

to replace `x * norm_unit x`

since that expression is used a lot and should have a name and is actually the whole point of `normalization_domain`

(we don't really care about the unit it multiplies by, right?).

But this would require lemmas from ring_theory/associated.lean about units and dvd.

Unfortunately, it imports data/int/gcd.lean which imports algebra.gcd_domain, and this is an essential import in the sense that a majority of the file is based on this import.

However, `data/int/gcd.lean`

is not an essential import of `ring_theory/associated.lean`

, in the sense that < 10% of the file breaks when I remove that import. Things that break include three theorems which is essentially examples about int and nat, and also a section below about normalization domain.

#### Kenny Lau (Feb 01 2019 at 12:21):

So my proposal is:

1. remove the import `data/int/gcd.lean`

from `ring_theory/associated.lean`

2. move `ring_theory/associated.lean`

to `algebra/associated.lean`

3. add the import `algebra/associated.lean`

to `algebra/gcd_domain.lean`

4. add `normalize`

in `algebra/gcd_domain.lean`

5. move the three theorems that break to `data/int/gcd.lean`

6. move the section that breaks to `algebra/gcd_domain.lean`

#### Kenny Lau (Feb 01 2019 at 12:21):

@Mario Carneiro do you think this is a good idea? did I miss anything?

#### Mario Carneiro (Feb 01 2019 at 12:23):

why does `int.gcd`

use `algebra.normalization_domain`

?

#### Kenny Lau (Feb 01 2019 at 12:24):

There is no `algebra.normalization_domain`

: it is just `algebra.gcd_domain`

.

#### Kenny Lau (Feb 01 2019 at 12:24):

And that uses that because the whole file is about gcd

#### Mario Carneiro (Feb 01 2019 at 12:24):

`nat.gcd`

doesn't

#### Kenny Lau (Feb 01 2019 at 12:24):

because `nat`

isn't a `gcd_domain`

#### Kenny Lau (Feb 01 2019 at 12:27):

I suppose we can remove the `normalization_domain`

and `gcd_domain`

sections of `data/int/gcd.lean`

and move them to `algebra/gcd_domain.lean`

?

#### Kenny Lau (Feb 01 2019 at 12:27):

What do you think?

#### Kenny Lau (Feb 01 2019 at 12:27):

afterall there's a proof that `int`

is `euclidean_domain`

in `algebra/euclidean_domain.lean`

anyway, so this wouldn't be unprecedented

#### Mario Carneiro (Feb 01 2019 at 12:28):

my guess is that you can do integer gcd by reference to nat gcd, without bringing in the abstract algebra. But setting that aside, I think that moving `ring_theory.associated`

to `algebra`

is okay for much of it, but not all; you will probably need to split the file

#### Kenny Lau (Feb 01 2019 at 12:29):

Ok I'll experiment on a branch

#### Mario Carneiro (Feb 01 2019 at 12:30):

I think that `data.int.gcd`

shouldn't bring in anything from `ring_theory`

#### Kenny Lau (Feb 01 2019 at 12:31):

I agree

#### Kenny Lau (Feb 01 2019 at 13:08):

@Mario Carneiro so where should these theorems go?

theorem irreducible_iff_nat_prime : ∀(a : ℕ), irreducible a ↔ nat.prime a lemma nat.prime_iff_prime {p : ℕ} : p.prime ↔ _root_.prime (p : ℕ) := lemma nat.prime_iff_prime_int {p : ℕ} : p.prime ↔ _root_.prime (p : ℤ) := def associates_int_equiv_nat : (associates ℤ) ≃ ℕ :=

#### Kenny Lau (Feb 01 2019 at 13:12):

https://github.com/leanprover-community/mathlib/blob/normalize/src/pending/default.lean

#### Kevin Buzzard (Feb 01 2019 at 14:59):

Can one break up file `X.lean`

into `X_part_1.lean`

and `X_part_2.lean`

and then just change `X.lean`

into `import X_part_1.lean import X_part_2.lean`

, and then you have more breathing space to fiddle with imports?

#### Kenny Lau (Feb 09 2019 at 21:55):

@Mario Carneiro what do you think about #668?

#### Mario Carneiro (Feb 09 2019 at 21:57):

what chris said - summary?

#### Kenny Lau (Feb 09 2019 at 22:02):

it's in this zulip thread

#### Mario Carneiro (Feb 09 2019 at 22:03):

some definitions changed?

#### Simon Hudon (Feb 09 2019 at 22:17):

I would chime in and say a Zulip thread is not a summary. It's useful for reference but you should be able to get the gist of the PR without looking at Zulip

#### Kenny Lau (Feb 09 2019 at 22:17):

done @Mario Carneiro

#### Chris Hughes (Feb 09 2019 at 22:46):

I think a good rule in future might be that moving stuff around should be in a separate PR from adding any new code, to make review easier.

#### Kenny Lau (Feb 09 2019 at 22:47):

agreed

#### Kenny Lau (Feb 09 2019 at 22:47):

I'll be careful about that in the future

Last updated: May 18 2021 at 17:44 UTC