where should these definitions live?

Stream: maths

[Anne Baanen]

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]

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]

I suggest starting ring_theory/polynomial/

[Johan Commelin]

@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]

That file is currently a hodge-podge of results.

[Johan Commelin]

I have a local branch with homogeneous.lean and symmetric.lean and those would also belong to that directory, I think.