# Zulip Chat Archive

## Stream: maths

### Topic: where should these definitions live?

#### Anne Baanen (Jun 25 2020 at 09:31):

I have a definition of and some lemmas about a polynomial `scale_roots p s`

, which has a root `r * s`

iff `p`

has a root `r`

and `s`

is not a zero divisor. I believe the best location for this is in `data/polynomial.lean`

, correct?

#### Anne Baanen (Jun 25 2020 at 09:31):

In that case I need to import `non_zero_divisors`

from `ring_theory/localization.lean`

, which depends on `data/polynomial.lean`

. So `non_zero_divisors R`

should be moved, but where? It cannot be with the definition of a domain in `algebra/ring.lean`

because `group_theory/submodule.lean`

depends on it indirectly.

#### Johan Commelin (Jun 25 2020 at 09:34):

I suggest starting `ring_theory/polynomial/`

#### Johan Commelin (Jun 25 2020 at 09:35):

@Anne Baanen You can move `ring_theory/polynomial.lean`

to `ring_theory/polynomial/basic.lean`

and add it as import to `default.lean`

, then the rest of mathlib shouldn't notice.

#### Johan Commelin (Jun 25 2020 at 09:35):

That file is currently a hodge-podge of results.

#### Johan Commelin (Jun 25 2020 at 09:36):

I have a local branch with `homogeneous.lean`

and `symmetric.lean`

and those would also belong to that directory, I think.

Last updated: May 12 2021 at 08:14 UTC