Where to cut this import chain

Stream: general

[Eric Wieser]

Items at the start of the list are imported by items at the end ofthe list:

['group_theory.perm.basic',
 'data.equiv.mul_add',
 'deprecated.group',
 'algebra.group_power.basic',
 'data.nat.basic',
 'data.nat.factorial',
 'data.list.perm',
 'tactic.wlog',
 'data.fintype.basic']

I want to import data.fintype.basic in group_theory.perm.basic, but I can't right now.

[Johan Commelin]

Maybe data.fintype.basic is too basic to use wlog?

[Johan Commelin]

But also wlog seems to have pretty heavy imports... otoh, I understand that it might want to know something about permutations.

[Johan Commelin]

But having tactic.wlog import all that seems quite much. I wonder if we can minimize something there.

[Eric Wieser]

Cutting deprecated.group out shouldn't be too hard

[Eric Wieser]

Although I suspec the cycle reappears somewhere else

[Reid Barton]

How about just adding a new file

[Rob Lewis]

wlog is used exactly once in fintype.basic so that would be an easy cut.

[Rob Lewis]

But also permutations in nat.basic seems a little much, no?

[Eric Wieser]

I think I'll try swapping the import direction between group_power.basic and deprecated.group

[Eric Wieser]

#5194

[Eric Wieser]

Reid Barton said:

How about just adding a new file

This is probably the right move to unblock me, but this import chain looks likely to cause pain in future.

[Eric Wieser]

For now, the fintype import is in equiv.perm.sign instead, #5201

[Eric Wieser]

I cut the import of perm.basic from mul_add in #5281 - which was enough to show me that perm.basic is used by fintype.basic directly anyway, making the rest of the import chain irrelevant.