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_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 (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
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
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
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