Is `quotient_group.quotient.fintype` a bad instance?

Stream: general

[Eric Wieser]

I found that if I import the file that defines docs#quotient_group.quotient.fintype first, then the current proof of docs#mul_action.card_modeq_card_fixed_points times out