## 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

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?

#### 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.

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