tracking down dependency chains

Stream: general

[Mario Carneiro]

Why does data.real.pi depend on data.finsupp? Are any of the current lean tools in a position to answer questions such as this?

[Mario Carneiro]

Could a tactic answer that question?

[Sebastien Gouezel]

You can do leanproject import-graph --from data.finsupp --to data.real.pi fins.pdf

[Sebastien Gouezel]

fins.pdf

[Sebastien Gouezel]

It shows that data.real.pi imports pretty much everything.

[Sebastien Gouezel]

That's a pretty nice file, by the way, with all the analysis on the left, all the algebra on the right, and then they merge cleanly to give you $\pi$.

[Yury G. Kudryashov]

Probably we should move parts of linear_algebra/basic depending on finsupp to another file.

[Yury G. Kudryashov]

Right now half of very basic linear_map/submodule theory is in algebra/module, and half is in linear_algebra/basic.

[Yury G. Kudryashov]

And the latter half is mixed with some preliminary pi/basis stuff that needs finsupp.

[Kevin Buzzard]

Lean pi quiz: which of the following things are needed to define pi in Lean.

• a) Riesz's Lemma
• b) Noetherian rings
• c) Tangent Cones
• d) Principal Ideal Domains
• e) All of the above.

[Kevin Buzzard]

We could have just made it $4/1-4/3+4/5-4/7+\cdots$ :-)

[Yury G. Kudryashov]

Another idea for a quiz. What was formalized earlier: Banach open mapping theorem or Rolle's theorem?

[Mario Carneiro]

Perfectoid spaces or single variable derivatives?

[Kevin Buzzard]

Bourbaki probably wrote books in a funny order too