# Zulip Chat Archive

## Stream: new members

### Topic: circular dependency problem

#### Moritz Firsching (Mar 13 2021 at 13:18):

When simplifying some bernoulli power series lemmas, I run into a dependency problem.

The pr is #6641. I have file `bernoulli_polynomial.lean`

depending on `bernoulli.lean`

. Some lemmas I moved from `bernoulli`

to `bernoulli_polynomial`

, because the new proof depends on stuff from `bernoulli_polynomial`

. However there are some other lemmas in `bernoulli`

, which depend on the lemmas that I moved to `bernoulli_polynomial`

. Should I then just move all the stuff that depends on the moved lemmas to `bernoulli_polynomial`

as well or is there a better way of doing it?

#### Bryan Gin-ge Chen (Mar 13 2021 at 15:24):

Yes, it looks like you'll have to move everything that depends on the moved declarations. If you anticipate that we may add a lot more to `bernoulli_polynomial.lean`

, it may make sense to create a 3rd file specific to Bernoulli power series and stuff that depends on those definitions, and at that point we may want to create a directory `number_theory/bernoulli/`

and rename `bernoulli.lean`

to `bernoulli/basic.lean`

, etc.

#### Heather Macbeth (Mar 13 2021 at 18:02):

I am not an expert here, but is there a reason it's in number theory, anyway? Many kinds of polynomials get their own file in `ring_theory/polynomial`

, see `chebyshev`

, `dickson`

, `symmetric`

, soon `pochhammer`

and `bernstein`

. Wouldn't it make sense to put `bernoulli`

there too?

#### Heather Macbeth (Mar 13 2021 at 18:03):

And the power series material could move to `ring_theory/power_series`

.

#### Alex J. Best (Mar 13 2021 at 18:35):

Certainly Mazur would put them in `math/bernoulli`

:grinning: http://people.math.harvard.edu/~mazur/papers/slides.Bartlett.pdf

#### Moritz Firsching (Mar 14 2021 at 12:55):

Thanks for all the hints! When trying to fix this, I noticed that I actually have a circular dependency in the proof, and this won't be resolve shifting stuff around between files..

I closed the pull request for now. When trying to simplify it I simply didn't realize that `bernoulli'_odd_eq_zero`

(written by @Ashvni Narayanan ) actually uses the power series we were trying to simplify...

Last updated: May 06 2021 at 22:13 UTC