circular imports in mathlib

Stream: maths

[Kevin Buzzard]

Johannes said in the p-adic PR

I'm fine with merging, with one exception: Please don't import topology in data/polynomial. I guess we need a analysis/polynomial.lean for the continuity statement.

I don't like this, as we get into a huge mess if we have too much cyclic dependencies between the top level directories. I think data shouldn't depend on analysis or the *_theory directories.

I've never thought about these issues. Are there general rules written down somewhere about what is acceptable and what is not when it comes to this sort of question?