circular dependency problem

Stream: new members

[Moritz Firsching]

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_polynomialas well or is there a better way of doing it?

[Bryan Gin-ge Chen]

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]

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]

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

[Alex J. Best]

Certainly Mazur would put them in math/bernoulli :grinning: http://people.math.harvard.edu/~mazur/papers/slides.Bartlett.pdf

[Moritz Firsching]

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