Promoting to polymorphic

Stream: mathlib4

[Bolton Bailey]

In this comment Eric tells me to golf an old theorem with my new theorem. But the old theorem is polymorphic over universes, and the new theorem relies on a prereq which is not. Should I promote the prereq? Demote the theorem I'm golfing?

[Yaël Dillies]

Why is any of your declarations non-universe polymorphic to start with?

[Yaël Dillies]

I would assume this is just a mistake you can fix.

[Bolton Bailey]

I'll check if anything breaks if I make exists_pow_ne_one_of_isCyclic polymorphic