Zulip Chat Archive

Stream: maths

Topic: where should these definitions live?


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 25 2020 at 09:34):

I suggest starting ring_theory/polynomial/

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jun 25 2020 at 09:35):

That file is currently a hodge-podge of results.

view this post on Zulip 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