Reduce imports to Analysis.LocallyConvex.Polar

Stream: general

[Ruben Van de Velde]

Ruben Van de Velde said:

I've poked at it a bit, will likely continue later. Might help with the longest pole as well

This is now #16479

[Ruben Van de Velde]

o.png

[Johan Commelin]

Great work! And still an impressive ratio of grey nodes left (-;

[Ruben Van de Velde]

#16489 should also help after I fix the merge conflict

[Ruben Van de Velde]

Ruben Van de Velde said:

#16489 should also help after I fix the merge conflict

Up for review

[Ruben Van de Velde]

o.png

[Yaël Dillies]

Why start at SetTheory.Cardinal.Basic, though? Can we see a bit more of the graph?

[Ruben Van de Velde]

That was the random part of mathlib that Kim was looking at upthread. A full dependency graph is rather too big to work with

[Yaël Dillies]

Sure yeah, I am just wondering whether there is another obviously wrong dependency we can easily cut out :wink:

[Kim Morrison]

Once we've finished cutting this chain we can move on to another one. :-)